Library classicaltypes

Require Import Coq.Logic.ClassicalFacts.
Require Import Classical.

Require Export types.

Lemma eq_undo: forall (A:Type) (x:A) (EQ:x=x), EQ=refl_equal x.

Theorem maptype_pi:
forall (A B:Type) (EQ1 EQ2:A=B) (x:A),
maptype EQ1 x=maptype EQ2 x.

Theorem eqtype_to_eq: prop_eqtype_to_eq.

Theorem maptype_selfany: forall (A:Type) (EQ:A=A) (x:A),
maptype EQ x=x.

Theorem eqtype_ind_self: forall (A:Type) (x:A) (P:A->Prop),
 P x -> forall y:A, x == y -> P y.

Theorem eqtype_rect_self: forall (A:Type) (x:A) (P:A->Type),
 P x -> forall y:A, x == y -> P y.