henkin cAnd

TimothyEarley · Jan 2, 2025 · 3b8edfc · 3b8edfc
1 parent 79575fd
commit 3b8edfc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/proof/Henkin.ard b/src/proof/Henkin.ard
@@ -47,7 +47,7 @@
     \lemma <->cAnd {_ : Language} {c : Context} {T : Theory c} {f g : Formula c}
       : Prf' T (cAnd f g) <-> (\Sigma (Prf' T f) (Prf' T g)) =>
       (
-        \lam p => {?},
+        \lam (inP h) => (inP (cAndElim1 h idp), inP (cAndElim2 h idp)),
         \lam (inP prf1, inP prf2) => inP (and prf1 prf2 idp)
       )
   }