Equality Eq refl;

repl : (A:*)(x:A)(y:A)(q:Eq _ _ x y)(P:(m:A)*)(p:P x)(P y);
intros;
by EqElim _ _ _ q;
fill p;
Qed;
Freeze repl;

trans : (A:*)(a:A)(b:A)(c:A)(p:Eq _ _ a b)(q:Eq _ _ b c)(Eq _ _ a c);
intros;
by EqElim _ _ _ q;
fill p;
Qed;
Freeze trans;

sym : (A:*)(a:A)(b:A)(p:Eq _ _ a b)(Eq _ _ b a);
intros;
by EqElim _ _ _ p;
refine refl;
Qed;
Freeze sym;

Repl Eq repl sym;

eq_resp_f:(A,B:*)(f:(a:A)B)(x:A)(y:A)(q:Eq _ _ x y)(Eq _ _ (f x) (f y));
intros;
by EqElim _ _ _ q;
refine refl;
Qed;
Freeze eq_resp_f;

Data Nat:* = O:Nat | S:(k:Nat)Nat;

plus' : (m:Nat)(n:Nat)<plus' m n : Nat>;
intro m;
induction m;
intros;
fill return n;
intros;
fill return (S (call <plus' k n0> (k_IH n0)));
Qed;

plus = [m:Nat][n:Nat](call <plus' m n> (plus' m n));

simplifyO:(n:Nat)(Eq _ _ (plus O n) n);
intros;
refine refl;
Qed;

simplifyS:(m,n:Nat)(Eq _ _ (plus (S m) n) (S (plus m n)));
intros;
refine refl;
Qed;

eq_resp_S:(n:Nat)(m:Nat)(q:Eq _ _ n m)(Eq _ _ (S n) (S m));
intros;
fill (eq_resp_f _ _ S n m q);
Qed;
Freeze eq_resp_S;

s_injective:(n:Nat)(m:Nat)(q:Eq _ _ (S n) (S m))(Eq _ _ n m);
intros;
local unS:(m:Nat)Nat;
intros;
induction m0;
fill n;
intros;
fill k;
fill eq_resp_f _ _ unS _ _ q;
Qed;
Freeze s_injective;

notO_S:(k:Nat)(not (Eq _ _ O (S k)));
intros;
equiv (q:Eq _ _ O (S k))False;
intros;
local dmotive : (x:Nat)(q:Eq _ _ O x)*;
intros;
induction x;
fill True;
intros;
fill False;
fill EqElim _ _ _ q dmotive II;
Qed;
Freeze notO_S;

notn_S:(n:Nat)(not (Eq _ n (S n)));
intro;
induction n;
fill notO_S O;
intros;
equiv (q:Eq _ (S k) (S (S k)))False;
intros;
claim q:Eq _ k (S k);
fill k_IH q0;
refine s_injective;
fill q;
Qed;
Freeze notn_S;

discriminate_Nat:(A:*)(k:Nat)(q:Eq _ O (S k))A;
intros;
local false:False;
fill notO_S k q;
induction false;
Qed;
Freeze discriminate_Nat;

plusnO:(n:Nat)(Eq _ _ (plus n O) n);
intro;
induction n;
refine refl;
intros;
equiv Eq _ _ (S (plus k O)) (S k);
refine eq_resp_S;
fill k_IH;
Qed;
Freeze plusnO;

plusnSm:(n:Nat)(m:Nat)(Eq _ _ (plus n (S m)) (S (plus n m)));
intros;
induction n;
refine refl;
intros;
refine eq_resp_S;
fill k_IH;
Qed;
Freeze plusnSm;

plus_comm:(n:Nat)(m:Nat)(Eq _ _ (plus n m) (plus m n));
intros;
induction n;
refine sym;
refine plusnO;
intros;
equiv Eq _ _ (S (plus k m)) (plus m (S k));
replace k_IH;
refine sym;
refine plusnSm;
Qed;
Freeze plus_comm;

plus_assoc:(m,n,p:Nat)(Eq _ _ (plus m (plus n p)) (plus (plus m n) p));
intros;
induction m;
refine refl;
intros;
equiv Eq _ _ (S (plus k (plus n p))) (plus (S (plus k n)) p);
replace k_IH;
refine refl;
Qed;
Freeze plus_assoc;

plus_eq_fst : (m,n,p:Nat)(q:Eq _ _ (plus p m) (plus p n))(Eq _ _ m n);
intro m n p;
induction p;
intros;
fill q;
intros;
refine k_IH;
refine s_injective;
refine q0;
Qed;
Freeze plus_eq_fst;

plus_eq_fst_sym : (m,n,p:Nat)(q:Eq _ _ (plus m p) (plus n p))(Eq _ _ m n);
intro m n p;
replace plus_comm m p;
replace plus_comm n p;
fill plus_eq_fst m n p;
Qed;
Freeze plus_eq_fst_sym;