proposition: Lemma wCon2Con : forall T : System, wConsistent T -> Consistent LNN T.
proof: Proof. intros T H; unfold wConsistent in H. unfold Consistent, Inconsistent; assert (H0: SysPrf T (exH 0, ~ ~ v#0 = v#0)%fol) by apply existSimp, nnI, eqRefl. assert (H1 : forall x : nat, In x (freeVarF (L:=LNN) (v#0 <> v#0)%fol) -> 0 = x) by (intros x H1; simpl in H1; repeat induction H1; auto). destruct (H _ _ H1 H0) as [x H2]; now exists (substF (v#0 <> v#0)%fol 0 (natToTerm x)). Qed.
imports: hydras.Ackermann(folProof folProp LNN) Coq(Arith List)