proposition: Lemma ModelConsistent (value : nat -> U M): (forall f : Formula L, mem _ T f -> interpFormula value (nnTranslate f)) -> Consistent L T.
proof: Proof. intros H; unfold Consistent; exists (v#O <> v#0)%fol. intros H0; assert (H1: interpFormula value (nnTranslate (v#O <> v#0)%fol)). { apply preserveValue. assumption. auto. } apply H1; simpl; auto. Qed.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)