Theorem: LO.Modal.Standard.Theory.iff_insert_ParametricConsistent (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (L)-Consistent insert p T ↔ ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (L)-Consistent insert p T → ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (L)-Consistent insert p T → ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
Tactic:
. intro h Γ hΓ;
  by_contra hC;
  have : L ⊬! p ⋏ List.conj' Γ ⟶ ⊥ := implyLeft_cons_conj'!.not.mp $ @h (p :: Γ) (by
    rintro q hq;
    simp at hq;
    cases hq with
    | inl h => subst h; simp;
    | inr h => simp; right; exact hΓ q h;
  );
  contradiction;
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
Tactic:
. intro h Γ hΓ;
  have := @h (Γ.remove p) (by
    intro q hq;
    have := by simpa using hΓ q $ List.mem_of_mem_remove hq;
    cases this with
    | inl h => simpa [h] using List.mem_remove_iff.mp hq;
    | inr h => assumption;
  );
  by_contra hC;
  have := imp_trans! andComm! $ implyLeftRemoveConj' (p := p) hC;
  contradiction;
State after:
no goals

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (L)-Consistent insert p T → ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
intro h Γ hΓ
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
⊢ L ⊬! p ⋏ Γ.conj' ⟶ ⊥

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
⊢ L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
by_contra hC
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Tactic:
have : L ⊬! p ⋏ List.conj' Γ ⟶ ⊥ := implyLeft_cons_conj'!.not.mp $ @h (p :: Γ) (by
  rintro q hq;
  simp at hq;
  cases hq with
  | inl h => subst h; simp;
  | inr h => simp; right; exact hΓ q h;
)
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
this : L ⊬! p ⋏ Γ.conj' ⟶ ⊥
⊢ False

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
this : L ⊬! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ ∀ p_1 ∈ p :: Γ, p_1 ∈ insert p T
Tactic:
rintro q hq
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ p :: Γ
⊢ q ∈ insert p T

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ p :: Γ
⊢ q ∈ insert p T
Tactic:
simp at hq
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
hq : q = p ∨ q ∈ Γ
⊢ q ∈ insert p T

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
hq : q = p ∨ q ∈ Γ
⊢ q ∈ insert p T
Tactic:
cases hq with
| inl h => subst h; simp;
| inr h => simp; right; exact hΓ q h;
State after:
no goals

State before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q = p
⊢ q ∈ insert p T
Tactic:
subst h
State after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
q : Formula α
h : (L)-Consistent insert q T
hC : L ⊢! q ⋏ Γ.conj' ⟶ ⊥
⊢ q ∈ insert q T

State before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
q : Formula α
h : (L)-Consistent insert q T
hC : L ⊢! q ⋏ Γ.conj' ⟶ ⊥
⊢ q ∈ insert q T
Tactic:
simp
State after:
no goals

State before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q ∈ Γ
⊢ q ∈ insert p T
Tactic:
simp
State after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q ∈ Γ
⊢ q = p ∨ q ∈ T

State before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q ∈ Γ
⊢ q = p ∨ q ∈ T
Tactic:
right
State after:
case inr.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q ∈ Γ
⊢ q ∈ T

State before:
case inr.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : (L)-Consistent insert p T
Γ : List (Formula α)
hΓ : ∀ q ∈ Γ, q ∈ T
hC : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
q : Formula α
h : q ∈ Γ
⊢ q ∈ T
Tactic:
exact hΓ q h
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
Tactic:
intro h Γ hΓ
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
⊢ L ⊬! Γ.conj' ⟶ ⊥

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
⊢ L ⊬! Γ.conj' ⟶ ⊥
Tactic:
have := @h (Γ.remove p) (by
  intro q hq;
  have := by simpa using hΓ q $ List.mem_of_mem_remove hq;
  cases this with
  | inl h => simpa [h] using List.mem_remove_iff.mp hq;
  | inr h => assumption;
)
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
⊢ L ⊬! Γ.conj' ⟶ ⊥

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
⊢ L ⊬! Γ.conj' ⟶ ⊥
Tactic:
by_contra hC
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
⊢ False

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
Tactic:
have := imp_trans! andComm! $ implyLeftRemoveConj' (p := p) hC
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this✝ : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
this : L ⊢! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
⊢ False

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
this✝ : L ⊬! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
this : L ⊢! p ⋏ (List.remove p Γ).conj' ⟶ ⊥
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
⊢ ∀ q ∈ List.remove p Γ, q ∈ T
Tactic:
intro q hq
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
⊢ q ∈ T

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
⊢ q ∈ T
Tactic:
have := by simpa using hΓ q $ List.mem_of_mem_remove hq;
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
this : q = p ∨ q ∈ T
⊢ q ∈ T

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
this : q = p ∨ q ∈ T
⊢ q ∈ T
Tactic:
cases this with
| inl h => simpa [h] using List.mem_remove_iff.mp hq;
| inr h => assumption;
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
⊢ ?m.55194
Tactic:
simpa using hΓ q $ List.mem_of_mem_remove hq
State after:
no goals

State before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
h : q = p
⊢ q ∈ T
Tactic:
simpa [h] using List.mem_remove_iff.mp hq
State after:
no goals

State before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
h✝ : ∀ {Γ : List (Formula α)}, (∀ q ∈ Γ, q ∈ T) → L ⊬! p ⋏ Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p T
q : Formula α
hq : q ∈ List.remove p Γ
h : q ∈ T
⊢ q ∈ T
Tactic:
assumption
State after:
no goals