definition hole : ∀A:Type.A → A ≝ λA.λx.x.
definition id : ∀A:Type.A → A ≝ λA.λx.x.
+(* Common case in dama, reduction with metas
+inductive list : Type := nil : list | cons : nat -> list -> list.
+let rec len l := match l with [ nil => O | cons _ l => S (len l) ].
+axiom lt : nat -> nat -> Prop.
+axiom foo : ∀x. Not (lt (hole ? x) (hole ? O)) = (lt x (len nil) -> False).
+*)
+
(* meta1 Vs meta2 with different contexts
axiom foo:
∀P:Type.∀f:P→P→Prop.∀x:P.
*)
alias num (instance 0) = "natural number".
-axiom foo: (12+12) = (12+11).
+axiom foo: (100+111) = (100+110).
(id ?(id ?(id ?(id ? (100+100))))) =