eq.neon

let eq (A : type) (x : A) (y : A) = 
    forall P : (A -> type) => P(x) -> P(y)

let refl_type = 
    forall (A: type) (a: A) => eq(A, a, a)

lemma refl : refl_type = 
    fun A x P px => px

let symm_type =
    forall (A: type) (x: A) (y: A) => eq(A,x,y) -> eq(A,y,x)

lemma symm : symm_type = 
    fun A x y xy P py => xy((fun z => P(z) -> P(x)), (fun px => px), py)

let trans_type = 
    forall (A: type) (x: A) (y: A) (z: A) => eq(A,x,y) -> eq(A,y,z) -> eq(A,x,z)

lemma trans : trans_type = 
    fun A x y z xy yz P px => yz(P, xy(P, px))

let subst_type = 
    forall (A: type) (P: A -> type) (x: A) (y: A) => eq(A,x,y) -> P(x) -> P(y)

lemma subst : subst_type = 
    fun A P x y xy => xy(P)


/** let refl (A : type) (x : A) (P : (A -> type)) (px : P(x)) = px */