include "logic/equality.ma".
+ninductive unit: Type[0] ≝ k: unit.
+
+ninductive bool: unit → Type[0] ≝ true : bool k | false : bool k.
+
+nlemma foo: true = false → False. #H; ndestruct;
+nqed.
+
(* nlemma prova : ∀T:Type[0].∀a,b:T.∀e:a = b.
∀P:∀x,y:T.x=y→Prop.P a a (refl T a) → P a b e.
#T;#a;#b;#e;#P;#H;