cExists intro

src/proof/PrfCorrect.ard

@@ -63,6 +63,18 @@
       \in rewrite h prf'
   | cAnd a toShow, and prf1 prf2 => \lam I m => (prfCorrectness prf1 I m, prfCorrectness prf2 I m)
   | toShow, modusPonens f prf1 prf2 => \lam I m => prfCorrectness prf2 I m (prfCorrectness prf1 I m)
+  | cExists toShow, cExistsIntro t prf => \lam I m =>
+      \let
+        h => prfCorrectness prf I m
+      \in inP (
+        Interpretation.evaluate I t,
+        models.fromSub.substitutionLemma-> {_} {suc c} {c} {toShow} I {extend I (evaluate I t)} {Substitution.substOne t}
+            (\lam (v : Fin (suc c)) => \case \elim v \with {
+              | 0 => idp
+              | suc f => idp
+            })
+            h
+      )
   \where {
     -- to work around termintation checking
 

src/proof/PrfFinite.ard

@@ -144,3 +144,7 @@
       FinSets.FinUnion h1.3 h2.3,
       modusPonens f (prfWeaken h1.4 (byLeft __)) (prfWeaken h2.4 (byRight __))
     )
+  | cExists toShow, cExistsIntro t prf =>
+    \let
+      | h => prfFinite prf
+    \in (h.1, h.2, h.3, cExistsIntro t h.4)

src/proof/PrfWeaken.ard

@@ -25,4 +25,5 @@
   | equal a b, fcong prfs pa pb => fcong (\lam i => prfWeaken (prfs i) sub) pa pb
   | atomic r terms, rcong prfs prf => rcong (\lam i => prfWeaken (prfs i) sub) (prfWeaken prf sub)
   | cAnd a b, and prf1 prf2 => and (prfWeaken prf1 sub) (prfWeaken prf2 sub)
-  | toShow, modusPonens f prf1 prf2 => modusPonens f (prfWeaken prf1 sub) (prfWeaken prf2 sub)
+  | toShow, modusPonens f prf1 prf2 => modusPonens f (prfWeaken prf1 sub) (prfWeaken prf2 sub)
+  | cExists f, cExistsIntro t prf => cExistsIntro t (prfWeaken prf sub)

src/proof/Proof.ard

@@ -41,6 +41,8 @@
 
   | cAnd a b => and (Prf axioms a) (Prf axioms b)
 
+  | cExists f => cExistsIntro (t : Term c) (prf : Prf axioms (Substitution.subst f t))
+
 
   -- TODO what is this rule?
   -- ¬(¬f -> g) = ¬(f ∨ g) = ¬f ∧ ¬g