How can I finish cases r here?

Stream: lean4

[MarcusArelius]

The case atom n has been done. But I Really do not know how to solve the case impl since the substitution p here is in Nat. Here is my code. The picture shows the problem.

inductive form : Type
| atom : Nat → form
| impl : form → form → form
| neg : form → form
| id : form → form → form

notation "#" n => form.atom n
notation p "⇒" q => form.impl p q
notation "~" p => form.neg p
notation p "≡" q => form.id p q
``````
inductive proof : form → Type
| ax1 : ∀ p q, proof (p ⇒ (q ⇒ p))
| ax2 : ∀ p q r, proof ((p ⇒ (q ⇒ r)) ⇒ ((p ⇒ q) ⇒ (p ⇒ r)))
| ax3 : ∀ p, proof (~~p ⇒ p)
| ax4 : ∀ p, proof (p ⇒ ~~p)
| ax5 : ∀ p q, proof ((~ p ⇒ ~ q) ⇒ (q ⇒ p))
| ax6 : ∀ p, proof (p ≡ p)
| ax7 : ∀ p q r, proof (((#p) ≡ q) ⇒ (r ⇒ r [p ↦ q ] ))
-- p is a Nat
| mp : ∀ p q, proof p → proof (p ⇒ q) → proof q


inductive tV : Type
| one : tV
| two : tV
| three : tV

structure model :=
  (interpretation : Nat → tV)
@[simp]
def tV.neg : tV → tV
  | tV.one => tV.two
  | _ => tV.one
@[simp]
def tV.impl : tV → tV → tV
  | tV.one, tV.two => tV.two
  | tV.one, tV.three => tV.two
  | _, _ => tV.one
@[simp]
def tV.id : tV → tV → tV
  | tV.one, tV.one => tV.one
  | tV.two, tV.two => tV.one
  | tV.three, tV.three => tV.one
  | _, _ => tV.three

def tV.form.substitution2 (src : tV) (_ : Nat) (_ : tV) : tV :=
  match src with
  | tV.one => tV.one
  | tV.two => tV.two
  | tV.three => tV.three
def sublemma (p q :tV):
  tV.impl (tV.id p q) (tV.impl p q) = tV.one
  := by cases p; cases q; repeat rfl; repeat cases q; repeat rfl

def reflemma (n: tV): tV.impl n n = tV.one
  := by cases n; repeat rfl

def idlemma (p :tV):
  tV.impl p tV.one = tV.one:= by cases p; repeat rfl

def subsublemma (p q n:tV):
  tV.impl (tV.id p q) (tV.impl n n) = tV.one
  :=
  by rw [reflemma]
     rw [idlemma]

theorem ax7_valid : ∀ p q r, model.valid (((#p) ≡ q) ⇒ (r ⇒ r [p ↦ q ] )) :=
by
intro p q r m
cases r with
| atom n => cases em ((#n) = # p) with
  | inl h => rw [h]
             have h1 : (#p)[p↦q]=q := by simp
             rw [h1]
             apply sublemma
  | inr h => have h2 : ¬(p=n):= by intro h1; rw [h1] at h; apply h; apply rfl
             have h3 : (#n)[p↦q]=#n := by simp; simp [h2]
             rw [h3]
             apply subsublemma

| impl p q => cases em ((p⇒q) = p) with

| neg p =>  sorry
| id p q =>  sorry

Impl-cases-1.png
impl-cases-2.png