feat(Propositional/Hilbert/F): prove DT_list, removing two sorries

`DT_list` (the deduction theorem for `List` contexts in the F-system) carried
two `sorry`s since the Hilbert-systems redesign (#812): the forward `ctx` case
and the backward `hcons` case. They transitively block `DT_finset` / `DT_set`,
which are proved via `DT_list`.

`Entailment.F` provides neither `HasAxiomImplyK` nor `HasAxiomImplyS`, so the
`Minimal`-layer `left_Conj₂!_intro` / `C_trans` are out of reach. This adds a
private helper `F_conj₂_mem` that builds `⋀Γ 🡒 φ` from `φ ∈ Γ` using only
F-level tools (`ruleI` transitivity + `and₁!`/`and₂!`), and fills both cases.

`#print axioms DT_list` → `[propext, Classical.choice, Quot.sound]` (no `sorryAx`).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: gotrevor

Foundation/Propositional/Hilbert/F/Deduction.lean

@@ -59,11 +59,25 @@ lemma deduct_conj {Γ : List (Formula α)} : Deduction H (Γ.toFinset) Γ.conj
       . simp;
       . exact ih;
 
+-- `Entailment.F` provides neither `HasAxiomImplyK` nor `HasAxiomImplyS`, so the
+-- `Minimal`-layer `left_Conj₂!_intro` / `C_trans` are out of reach. We instead build
+-- `⋀Γ 🡒 φ` from `φ ∈ Γ` using only F-level tools: `ruleI` (transitivity) and `and₁!`/`and₂!`.
+private lemma F_conj₂_mem {Γ : List (Formula α)} (h : φ ∈ Γ) : H ⊢ Γ.conj₂ 🡒 φ := by
+  induction Γ using List.induction_with_singleton with
+  | hnil => simp at h;
+  | hsingle ψ => simp only [List.mem_singleton] at h; subst h; simpa using impId;
+  | hcons ψ Δ he ih =>
+    rw [List.conj₂_cons_nonempty he];
+    simp only [List.mem_cons] at h;
+    rcases h with rfl | h;
+    . simp;
+    . apply ruleI ?_ (ih h); simp;
+
 lemma DT_list {Γ : List (Formula α)} : (Deduction H Γ.toFinset φ) ↔ H ⊢ Γ.conj₂ 🡒 φ := by
   constructor;
   . intro h;
     induction h with
-    | ctx hφ => sorry;
+    | ctx hφ => exact F_conj₂_mem (List.mem_toFinset.mp hφ);
     | thm hφ => apply af hφ;
     | mp => grind;
     | andIR => apply CK_of_C_of_C <;> assumption;
@@ -78,7 +92,13 @@ lemma DT_list {Γ : List (Formula α)} : (Deduction H Γ.toFinset φ) ↔ H ⊢
       apply Deduction.ctx;
       simp;
     | hcons ψ Γ hΓ ih =>
-      sorry;
+      rw [List.conj₂_cons_nonempty hΓ] at h;
+      apply Deduction.mp h;
+      apply Deduction.andIR;
+      . apply Deduction.ctx; simp;
+      . apply deduction_subset (Γ₁ := Γ.toFinset);
+        . simp;
+        . exact deduct_conj;
 
 lemma DT_finset {Γ : Finset (Formula α)} : (Deduction H Γ φ) ↔ (H ⊢ Γ.conj 🡒 φ) := by simpa [Finset.conj] using DT_list (Γ := Γ.toList);