Theorem: repl_in_P_equiv (Pdl/Substitution.lean)

State before:
α1 α2 : Program
x : ℕ
ψ : Formula
⊢ α1≡ᵣα2 → repl_in_P x ψ α1≡ᵣrepl_in_P x ψ α2
Tactic:
intro hyp
State after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
⊢ repl_in_P x ψ α1≡ᵣrepl_in_P x ψ α2

State before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
⊢ repl_in_P x ψ α1≡ᵣrepl_in_P x ψ α2
Tactic:
intro W M w v
State after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v

State before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v
Tactic:
have claim1 := repl_in_model_rel_iff x ψ α1 M w v
State after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v

State before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v
Tactic:
have claim2 := repl_in_model_rel_iff x ψ α2 M w v
State after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v

State before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v
Tactic:
rw [claim1]
State after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate (repl_in_model x ψ M) α1 w v ↔ relate M (repl_in_P x ψ α2) w v

State before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate (repl_in_model x ψ M) α1 w v ↔ relate M (repl_in_P x ψ α2) w v
Tactic:
rw [claim2]
State after:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate (repl_in_model x ψ M) α1 w v ↔ relate (repl_in_model x ψ M) α2 w v

State before:
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
claim1 : relate M (repl_in_P x ψ α1) w v ↔ relate (repl_in_model x ψ M) α1 w v
claim2 : relate M (repl_in_P x ψ α2) w v ↔ relate (repl_in_model x ψ M) α2 w v
⊢ relate (repl_in_model x ψ M) α1 w v ↔ relate (repl_in_model x ψ M) α2 w v
Tactic:
apply hyp
State after:
no goals