fact: Definition f0 : Formula LNN := forallH 0 (orH (equal (var 0) Zero) (existH 1 (equal (var 0) (apply (Languages.Succ_ : Functions LNN) (Tcons (var 1) (@Tnil _)))))).
imports: Coq(Arith Lists.List) fol folProp Languages LNN folProof