1. Paweł Wieczorek
  2. Metalogic

Commits

Paweł Wieczorek  committed fccdb8e

  • Participants
  • Parent commits 7b29c72
  • Branches default

Comments (0)

Files changed (1)

File metalogic/Fol/TheoremModelExistence.v

View file
  • Ignore whitespace
 exists t.
 destruct Ht.
 destruct H1.
-split; eauto with metalogic_db.
+split. auto.
 
-apply FolModelExistence''.
+eauto 3 with metalogic_db sets.
+
+assert (exists M, L @ M ||= T').
+apply FolModelExistence''; auto.
+destruct H.
+exists x.
+eauto with metalogic_db sets.
 Qed.
 
 (**************************************************************************