fact: Example f3 := (orH (equal (var 0) (apply LNN Zero_ Tnil)) (existH 1 (equal (var 0) (apply LNN Succ_ (Tcons (var 1) Tnil))))).
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)