+(* 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).
+*)
+