Theorem: Lean4Lean.VExpr.skips_iff (Lean4Lean/Theory/VExpr.lean)

State before:
case zero
k : Nat
e : VExpr
⊢ Skips e Nat.zero k ↔ Skips' Nat.zero e k
Tactic:
simp [Skips, unliftN]
State after:
case zero
k : Nat
e : VExpr
⊢ Skips' 0 e k

State before:
case zero
k : Nat
e : VExpr
⊢ Skips' 0 e k
Tactic:
induction e generalizing k <;> simp [Skips', *]
State after:
no goals

State before:
case succ
k n : Nat
ih : ∀ {e : VExpr}, Skips e n k ↔ Skips' n e k
e : VExpr
⊢ Skips e (Nat.succ n) k ↔ Skips' (Nat.succ n) e k
Tactic:
simp [Nat.succ_eq_add_one, skips_add, ih]
State after:
case succ
k n : Nat
ih : ∀ {e : VExpr}, Skips e n k ↔ Skips' n e k
e : VExpr
⊢ (∃ e', Skips' n e' k ∧ e = liftN 1 e' k) ↔ Skips' (n + 1) e k

State before:
case succ
k n : Nat
ih : ∀ {e : VExpr}, Skips e n k ↔ Skips' n e k
e : VExpr
⊢ (∃ e', Skips' n e' k ∧ e = liftN 1 e' k) ↔ Skips' (n + 1) e k
Tactic:
clear ih
State after:
case succ
k n : Nat
e : VExpr
⊢ (∃ e', Skips' n e' k ∧ e = liftN 1 e' k) ↔ Skips' (n + 1) e k

State before:
case succ.bvar
n i k : Nat
⊢ (∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k) ↔ Skips' (n + 1) (bvar i) k
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, fun h => ?_⟩
State after:
case succ.bvar.refine_1
n i k : Nat
x✝ : ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : bvar i = liftN 1 e' k
⊢ Skips' (n + 1) (bvar i) k

case succ.bvar.refine_2
n i k : Nat
h : Skips' (n + 1) (bvar i) k
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k

State before:
case succ.bvar.refine_1
n i k : Nat
x✝ : ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : bvar i = liftN 1 e' k
⊢ Skips' (n + 1) (bvar i) k
Tactic:
cases e' <;> cases h2
State after:
case succ.bvar.refine_1.bvar.refl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
⊢ Skips' (n + 1) (bvar (liftVar 1 deBruijnIndex✝ k)) k

State before:
case succ.bvar.refine_1.bvar.refl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
⊢ Skips' (n + 1) (bvar (liftVar 1 deBruijnIndex✝ k)) k
Tactic:
simp [Skips', liftVar]
State after:
case succ.bvar.refine_1.bvar.refl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
⊢ (if deBruijnIndex✝ < k then deBruijnIndex✝ else 1 + deBruijnIndex✝) < k + (n + 1) →
    (if deBruijnIndex✝ < k then deBruijnIndex✝ else 1 + deBruijnIndex✝) < k

State before:
case succ.bvar.refine_1.bvar.refl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
⊢ (if deBruijnIndex✝ < k then deBruijnIndex✝ else 1 + deBruijnIndex✝) < k + (n + 1) →
    (if deBruijnIndex✝ < k then deBruijnIndex✝ else 1 + deBruijnIndex✝) < k
Tactic:
split
State after:
case succ.bvar.refine_1.bvar.refl.inl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : deBruijnIndex✝ < k
⊢ deBruijnIndex✝ < k + (n + 1) → deBruijnIndex✝ < k

case succ.bvar.refine_1.bvar.refl.inr
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : ¬deBruijnIndex✝ < k
⊢ 1 + deBruijnIndex✝ < k + (n + 1) → 1 + deBruijnIndex✝ < k

State before:
case succ.bvar.refine_1.bvar.refl.inl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : deBruijnIndex✝ < k
⊢ deBruijnIndex✝ < k + (n + 1) → deBruijnIndex✝ < k
Tactic:
intro
State after:
case succ.bvar.refine_1.bvar.refl.inl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : deBruijnIndex✝ < k
a✝ : deBruijnIndex✝ < k + (n + 1)
⊢ deBruijnIndex✝ < k

State before:
case succ.bvar.refine_1.bvar.refl.inl
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : deBruijnIndex✝ < k
a✝ : deBruijnIndex✝ < k + (n + 1)
⊢ deBruijnIndex✝ < k
Tactic:
assumption
State after:
no goals

State before:
case succ.bvar.refine_1.bvar.refl.inr
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h✝ : ¬deBruijnIndex✝ < k
⊢ 1 + deBruijnIndex✝ < k + (n + 1) → 1 + deBruijnIndex✝ < k
Tactic:
next h2 =>
rw [Nat.add_comm, ← Nat.add_assoc, Nat.succ_lt_succ_iff]
exact fun h => h2.elim (h1 h)
State after:
no goals

State before:
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h2 : ¬deBruijnIndex✝ < k
⊢ 1 + deBruijnIndex✝ < k + (n + 1) → 1 + deBruijnIndex✝ < k
Tactic:
rw [Nat.add_comm, ← Nat.add_assoc, Nat.succ_lt_succ_iff]
State after:
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h2 : ¬deBruijnIndex✝ < k
⊢ deBruijnIndex✝ < k + n → deBruijnIndex✝ + 1 < k

State before:
n k deBruijnIndex✝ : Nat
h1 : Skips' n (bvar deBruijnIndex✝) k
x✝ : ∃ e', Skips' n e' k ∧ bvar (liftVar 1 deBruijnIndex✝ k) = liftN 1 e' k
h2 : ¬deBruijnIndex✝ < k
⊢ deBruijnIndex✝ < k + n → deBruijnIndex✝ + 1 < k
Tactic:
exact fun h => h2.elim (h1 h)
State after:
no goals

State before:
case succ.bvar.refine_2
n i k : Nat
h : Skips' (n + 1) (bvar i) k
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
Tactic:
simp [Skips'] at h
State after:
case succ.bvar.refine_2
n i k : Nat
h : i < k + (n + 1) → i < k
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k

State before:
n i k : Nat
h : i < k + (n + 1) → i < k
h' : i < k + n + 1
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
Tactic:
exact ⟨.bvar i, fun _ => h h', by simp [liftN, liftVar, h h']⟩
State after:
no goals

State before:
n i k : Nat
h : i < k + (n + 1) → i < k
h' : i < k + n + 1
⊢ bvar i = liftN 1 (bvar i) k
Tactic:
simp [liftN, liftVar, h h']
State after:
no goals

State before:
n i k : Nat
h : i < k + (n + 1) → i < k
h' : ¬i < k + n + 1
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
Tactic:
have := Nat.not_lt.1 h'
State after:
n i k : Nat
h : i < k + (n + 1) → i < k
h' : ¬i < k + n + 1
this : k + n + 1 ≤ i
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k

State before:
n i k : Nat
h : i < k + (n + 1) → i < k
h' : ¬i < k + n + 1
this : k + n + 1 ≤ i
⊢ ∃ e', Skips' n e' k ∧ bvar i = liftN 1 e' k
Tactic:
let i+1 := i
State after:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i + 1 < k + n + 1
this : k + n + 1 ≤ i + 1
⊢ ∃ e', Skips' n e' k ∧ bvar (i + 1) = liftN 1 e' k

State before:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i + 1 < k + n + 1
this : k + n + 1 ≤ i + 1
⊢ ∃ e', Skips' n e' k ∧ bvar (i + 1) = liftN 1 e' k
Tactic:
rw [Nat.add_lt_add_iff_right] at h'
State after:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i < k + n
this : k + n + 1 ≤ i + 1
⊢ ∃ e', Skips' n e' k ∧ bvar (i + 1) = liftN 1 e' k

State before:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i < k + n
this✝ : k + n + 1 ≤ i + 1
this : ¬i < k
⊢ ∃ e', Skips' n e' k ∧ bvar (i + 1) = liftN 1 e' k
Tactic:
exact ⟨.bvar i, h'.elim, by simp [liftN, liftVar]; rw [if_neg this, Nat.add_comm]⟩
State after:
no goals

State before:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i < k + n
this✝ : k + n + 1 ≤ i + 1
this : ¬i < k
⊢ bvar (i + 1) = liftN 1 (bvar i) k
Tactic:
simp [liftN, liftVar]
State after:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i < k + n
this✝ : k + n + 1 ≤ i + 1
this : ¬i < k
⊢ i + 1 = if i < k then i else 1 + i

State before:
n i✝ k i : Nat
h : i + 1 < k + (n + 1) → i + 1 < k
h' : ¬i < k + n
this✝ : k + n + 1 ≤ i + 1
this : ¬i < k
⊢ i + 1 = if i < k then i else 1 + i
Tactic:
rw [if_neg this, Nat.add_comm]
State after:
no goals

State before:
case succ.sort
n : Nat
u : VLevel
k : Nat
⊢ (∃ e', Skips' n e' k ∧ sort u = liftN 1 e' k) ↔ Skips' (n + 1) (sort u) k
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, fun _ => ⟨.sort u, by simp [Skips', liftN]⟩⟩
State after:
case succ.sort
n : Nat
u : VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ sort u = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : sort u = liftN 1 e' k
⊢ Skips' (n + 1) (sort u) k

State before:
case succ.sort
n : Nat
u : VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ sort u = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : sort u = liftN 1 e' k
⊢ Skips' (n + 1) (sort u) k
Tactic:
cases e' <;> cases h2
State after:
case succ.sort.sort.refl
n : Nat
u : VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ sort u = liftN 1 e' k
h1 : Skips' n (sort u) k
⊢ Skips' (n + 1) (sort u) k

State before:
case succ.sort.sort.refl
n : Nat
u : VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ sort u = liftN 1 e' k
h1 : Skips' n (sort u) k
⊢ Skips' (n + 1) (sort u) k
Tactic:
simp [Skips']
State after:
no goals

State before:
n : Nat
u : VLevel
k : Nat
x✝ : Skips' (n + 1) (sort u) k
⊢ Skips' n (sort u) k ∧ sort u = liftN 1 (sort u) k
Tactic:
simp [Skips', liftN]
State after:
no goals

State before:
case succ.const
n : Nat
c : Name
ls : List VLevel
k : Nat
⊢ (∃ e', Skips' n e' k ∧ const c ls = liftN 1 e' k) ↔ Skips' (n + 1) (const c ls) k
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, fun _ => ⟨.const c ls, by simp [Skips', liftN]⟩⟩
State after:
case succ.const
n : Nat
c : Name
ls : List VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ const c ls = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : const c ls = liftN 1 e' k
⊢ Skips' (n + 1) (const c ls) k

State before:
case succ.const
n : Nat
c : Name
ls : List VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ const c ls = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : const c ls = liftN 1 e' k
⊢ Skips' (n + 1) (const c ls) k
Tactic:
cases e' <;> cases h2
State after:
case succ.const.const.refl
n : Nat
c : Name
ls : List VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ const c ls = liftN 1 e' k
h1 : Skips' n (const c ls) k
⊢ Skips' (n + 1) (const c ls) k

State before:
case succ.const.const.refl
n : Nat
c : Name
ls : List VLevel
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ const c ls = liftN 1 e' k
h1 : Skips' n (const c ls) k
⊢ Skips' (n + 1) (const c ls) k
Tactic:
simp [Skips']
State after:
no goals

State before:
n : Nat
c : Name
ls : List VLevel
k : Nat
x✝ : Skips' (n + 1) (const c ls) k
⊢ Skips' n (const c ls) k ∧ const c ls = liftN 1 (const c ls) k
Tactic:
simp [Skips', liftN]
State after:
no goals

State before:
case succ.app
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k) ↔ Skips' (n + 1) (app f a) k
Tactic:
simp [Skips', ← fIH, ← aIH]
State after:
case succ.app
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ a = liftN 1 e' k

State before:
case succ.app
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ a = liftN 1 e' k
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, ?_⟩
State after:
case succ.app.refine_1
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : app f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ a = liftN 1 e' k

case succ.app.refine_2
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ ((∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ a = liftN 1 e' k) →
    ∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k

State before:
case succ.app.refine_1
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : app f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ a = liftN 1 e' k
Tactic:
cases e' <;> cases h2
State after:
case succ.app.refine_1.app.refl
n k : Nat
fn✝ arg✝ : VExpr
h1 : Skips' n (app fn✝ arg✝) k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 fn✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 fn✝ k) k_1
aIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 arg✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 arg✝ k) k_1
x✝ : ∃ e', Skips' n e' k ∧ app (liftN 1 fn✝ k) (liftN 1 arg✝ k) = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ liftN 1 fn✝ k = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ liftN 1 arg✝ k = liftN 1 e' k

State before:
case succ.app.refine_1.app.refl
n k : Nat
fn✝ arg✝ : VExpr
h1 : Skips' n (app fn✝ arg✝) k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 fn✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 fn✝ k) k_1
aIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 arg✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 arg✝ k) k_1
x✝ : ∃ e', Skips' n e' k ∧ app (liftN 1 fn✝ k) (liftN 1 arg✝ k) = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ liftN 1 fn✝ k = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ liftN 1 arg✝ k = liftN 1 e' k
Tactic:
exact ⟨⟨_, h1.1, rfl⟩, ⟨_, h1.2, rfl⟩⟩
State after:
no goals

State before:
case succ.app.refine_2
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ ((∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' k ∧ a = liftN 1 e' k) →
    ∃ e', Skips' n e' k ∧ app f a = liftN 1 e' k
Tactic:
rintro ⟨⟨e1, h1, rfl⟩, ⟨e2, h2, rfl⟩⟩
State after:
case succ.app.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 k
aIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 k) k_1
⊢ ∃ e', Skips' n e' k ∧ app (liftN 1 e1 k) (liftN 1 e2 k) = liftN 1 e' k

State before:
case succ.app.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 k
aIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 k) k_1
⊢ ∃ e', Skips' n e' k ∧ app (liftN 1 e1 k) (liftN 1 e2 k) = liftN 1 e' k
Tactic:
exact ⟨.app .., ⟨h1, h2⟩, rfl⟩
State after:
no goals

State before:
case succ.forallE
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ forallE f a = liftN 1 e' k) ↔ Skips' (n + 1) (forallE f a) k
Tactic:
simp [Skips', ← fIH, ← aIH]
State after:
case succ.forallE
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ forallE f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)

State before:
case succ.forallE
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ forallE f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, ?_⟩
State after:
case succ.forallE.refine_1
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ forallE f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : forallE f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)

case succ.forallE.refine_2
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ ((∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)) →
    ∃ e', Skips' n e' k ∧ forallE f a = liftN 1 e' k

State before:
case succ.forallE.refine_1
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ forallE f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : forallE f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)
Tactic:
cases e' <;> cases h2
State after:
case succ.forallE.refine_1.forallE.refl
n k : Nat
binderType✝ body✝ : VExpr
h1 : Skips' n (forallE binderType✝ body✝) k
fIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 binderType✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 binderType✝ k) k_1
aIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 body✝ (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 body✝ (k + 1)) k_1
x✝ : ∃ e', Skips' n e' k ∧ forallE (liftN 1 binderType✝ k) (liftN 1 body✝ (k + 1)) = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ liftN 1 binderType✝ k = liftN 1 e' k) ∧
    ∃ e', Skips' n e' (k + 1) ∧ liftN 1 body✝ (k + 1) = liftN 1 e' (k + 1)

State before:
case succ.forallE.refine_1.forallE.refl
n k : Nat
binderType✝ body✝ : VExpr
h1 : Skips' n (forallE binderType✝ body✝) k
fIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 binderType✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 binderType✝ k) k_1
aIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 body✝ (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 body✝ (k + 1)) k_1
x✝ : ∃ e', Skips' n e' k ∧ forallE (liftN 1 binderType✝ k) (liftN 1 body✝ (k + 1)) = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ liftN 1 binderType✝ k = liftN 1 e' k) ∧
    ∃ e', Skips' n e' (k + 1) ∧ liftN 1 body✝ (k + 1) = liftN 1 e' (k + 1)
Tactic:
exact ⟨⟨_, h1.1, rfl⟩, ⟨_, h1.2, rfl⟩⟩
State after:
no goals

State before:
case succ.forallE.refine_2
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ ((∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)) →
    ∃ e', Skips' n e' k ∧ forallE f a = liftN 1 e' k
Tactic:
rintro ⟨⟨e1, h1, rfl⟩, ⟨e2, h2, rfl⟩⟩
State after:
case succ.forallE.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 (k + 1)
aIH :
  ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 (k + 1)) k_1
⊢ ∃ e', Skips' n e' k ∧ forallE (liftN 1 e1 k) (liftN 1 e2 (k + 1)) = liftN 1 e' k

State before:
case succ.forallE.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 (k + 1)
aIH :
  ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 (k + 1)) k_1
⊢ ∃ e', Skips' n e' k ∧ forallE (liftN 1 e1 k) (liftN 1 e2 (k + 1)) = liftN 1 e' k
Tactic:
exact ⟨.forallE .., ⟨h1, h2⟩, rfl⟩
State after:
no goals

State before:
case succ.lam
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ lam f a = liftN 1 e' k) ↔ Skips' (n + 1) (lam f a) k
Tactic:
simp [Skips', ← fIH, ← aIH]
State after:
case succ.lam
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ lam f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)

State before:
case succ.lam
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ (∃ e', Skips' n e' k ∧ lam f a = liftN 1 e' k) ↔
    (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)
Tactic:
refine ⟨fun ⟨e', h1, h2⟩ => ?_, ?_⟩
State after:
case succ.lam.refine_1
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ lam f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : lam f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)

case succ.lam.refine_2
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ ((∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)) →
    ∃ e', Skips' n e' k ∧ lam f a = liftN 1 e' k

State before:
case succ.lam.refine_1
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
x✝ : ∃ e', Skips' n e' k ∧ lam f a = liftN 1 e' k
e' : VExpr
h1 : Skips' n e' k
h2 : lam f a = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)
Tactic:
cases e' <;> cases h2
State after:
case succ.lam.refine_1.lam.refl
n k : Nat
binderType✝ body✝ : VExpr
h1 : Skips' n (lam binderType✝ body✝) k
fIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 binderType✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 binderType✝ k) k_1
aIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 body✝ (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 body✝ (k + 1)) k_1
x✝ : ∃ e', Skips' n e' k ∧ lam (liftN 1 binderType✝ k) (liftN 1 body✝ (k + 1)) = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ liftN 1 binderType✝ k = liftN 1 e' k) ∧
    ∃ e', Skips' n e' (k + 1) ∧ liftN 1 body✝ (k + 1) = liftN 1 e' (k + 1)

State before:
case succ.lam.refine_1.lam.refl
n k : Nat
binderType✝ body✝ : VExpr
h1 : Skips' n (lam binderType✝ body✝) k
fIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 binderType✝ k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 binderType✝ k) k_1
aIH :
  ∀ {k_1 : Nat},
    (∃ e', Skips' n e' k_1 ∧ liftN 1 body✝ (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 body✝ (k + 1)) k_1
x✝ : ∃ e', Skips' n e' k ∧ lam (liftN 1 binderType✝ k) (liftN 1 body✝ (k + 1)) = liftN 1 e' k
⊢ (∃ e', Skips' n e' k ∧ liftN 1 binderType✝ k = liftN 1 e' k) ∧
    ∃ e', Skips' n e' (k + 1) ∧ liftN 1 body✝ (k + 1) = liftN 1 e' (k + 1)
Tactic:
exact ⟨⟨_, h1.1, rfl⟩, ⟨_, h1.2, rfl⟩⟩
State after:
no goals

State before:
case succ.lam.refine_2
n : Nat
f a : VExpr
fIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ↔ Skips' (n + 1) f k
aIH : ∀ {k : Nat}, (∃ e', Skips' n e' k ∧ a = liftN 1 e' k) ↔ Skips' (n + 1) a k
k : Nat
⊢ ((∃ e', Skips' n e' k ∧ f = liftN 1 e' k) ∧ ∃ e', Skips' n e' (k + 1) ∧ a = liftN 1 e' (k + 1)) →
    ∃ e', Skips' n e' k ∧ lam f a = liftN 1 e' k
Tactic:
rintro ⟨⟨e1, h1, rfl⟩, ⟨e2, h2, rfl⟩⟩
State after:
case succ.lam.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 (k + 1)
aIH :
  ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 (k + 1)) k_1
⊢ ∃ e', Skips' n e' k ∧ lam (liftN 1 e1 k) (liftN 1 e2 (k + 1)) = liftN 1 e' k

State before:
case succ.lam.refine_2.intro.intro.intro.intro.intro
n k : Nat
e1 : VExpr
h1 : Skips' n e1 k
fIH : ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e1 k = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e1 k) k_1
e2 : VExpr
h2 : Skips' n e2 (k + 1)
aIH :
  ∀ {k_1 : Nat}, (∃ e', Skips' n e' k_1 ∧ liftN 1 e2 (k + 1) = liftN 1 e' k_1) ↔ Skips' (n + 1) (liftN 1 e2 (k + 1)) k_1
⊢ ∃ e', Skips' n e' k ∧ lam (liftN 1 e1 k) (liftN 1 e2 (k + 1)) = liftN 1 e' k
Tactic:
exact ⟨.lam .., ⟨h1, h2⟩, rfl⟩
State after:
no goals