Commits

Paweł Wieczorek committed 7b29c72

Comments (0)

Files changed (1)

metalogic/Fol/TheoremModelExistence.v

 Require Import String.
 Require Import FunctionalExtensionality.
 
-(**------------------------------------------------------------------------
+(**************************************************************************
  *
 
 Module Type WitnessExtensionDef. 
 red.
 red in wconsT.
 intros.
-destruct wconsT with p x as [t Ht]; auto .
+destruct wconsT with p x as [t Ht Htt]; auto .
 exists t.
-eauto with metalogic_db sets.
+destruct Ht.
+destruct H1.
+split; eauto with metalogic_db.
 
 apply FolModelExistence''.
 Qed.
 
+(**************************************************************************
+ * TWIERDZENIE O ISTNIENIU MODELU.
+ * Teoria T ma model gdy jest niesprzeczna.
+ *)
+
 Theorem FolModelExistence : forall L (T:FolPropSet L),
         FolConsistent T -> exists M, L@M ||= T.
 Proof.