Eq = λA::*.λB::*.∀P::* ⇒ *.P A → P B; refl : ∀A.Eq A A = ΛA::*.ΛP::*⇒*.λx:P A.x; symm = ΛA::*.ΛB::*.λe:Eq A B.e [λX::*.Eq X A] (refl [A]); trans = ΛA::*.ΛB::*.ΛC::*.λab:Eq A B.λbc:Eq B C. bc [Eq A] ab; lift = ΛA::*.ΛB::*.ΛP::* ⇒ *.λe:Eq A B.e [λX::*.Eq (P A) (P X)] (refl [P A]);