Module misc

Implicit Arguments On.

Hints Resolve sym_eqT : sym.

Theorem congr : (a,b:Type; h:a->b; u,v:a) (u == v) -> (h u) == (h v).
Proof.
Induction 1; Reflexivity.
Qed.

Theorem congr2 : (a,b,c:Type; h:a->b->c; u,v:a; s,t:b)
  u==v -> s==t -> (h u s) == (h v t).
Proof.
Intros; Case H; Case H0; Reflexivity.
Qed.

Theorem plug : (a: Type; h:a->a; u,v : a)(u == v) -> (h u) == (h v).
Induction 1; Reflexivity.
Proof.
Qed.
Hints Resolve plug.

Theorem plug2 : (a:Type; h:a->a->a; u,v:a; s,t:a)
  u==v -> s==t -> (h u s) == (h v t).
Proof.
Intros; Case H; Case H0; Reflexivity.
Qed.
Hints Resolve plug2.

Inductive Star : Type := star_intro : Star.
Definition pointer [A:Type; x:A; s:Star] : A :=
  Cases s of star_intro => x end.

Section Sum.
  Variable A,B:Type.

  Inductive Sum : Type :=
    | sum1 : A->Sum
    | sum2 : B->Sum.
End Sum.

Section Pair.
  Variables A,B:Type.

  Inductive Prod : Type := pair : A->B->Prod.

  Definition pair1 [x:Prod] : A :=
    Cases x of (pair a _) => a end.

  Definition pair2 [x:Prod] : B :=
    Cases x of (pair _ b) => b end.
End Pair.

Axiom extensionality : (x:Type; f:x-> Type; u,v: (y:x)(f y))
  ((y:x)(u y) == (v y)) -> u == v.

Lemma nondep_extensionality : (a,b:Type; u,v:a->b)
  ((x:a)(u x) == (v x)) -> u == v.
Proof.
Intros.
Apply extensionality with f:=[x:a]b.
Assumption.
Qed.
Hints Resolve nondep_extensionality.

Axiom proof_irrelevance : (P : Prop; p,q: P)(p == q).

Definition type_of := [T:Type; t:T]T.