proposition: Lemma minimal_def : minimal = (fun _6536 : nat -> Prop => @ε nat (fun n : nat => (_6536 n) /\ (forall m : nat, (Peano.lt m n) -> ~ (_6536 m)))).
proof: Proof. exact (eq_refl minimal). Qed.
imports: coq theory_hol types