Theorem: HTPI.seq_cons_one_one (HTPILib/Chap8Part2.lean)

State before:
U : Type
⊢ one_to_one (seq_cons U)
Tactic:
fix (a1, l1) : U × List U
State after:
U : Type
a1 : U
l1 : List U
⊢ ∀ (x2 : U × List U), seq_cons U (a1, l1) = seq_cons U x2 → (a1, l1) = x2

State before:
U : Type
a1 : U
l1 : List U
⊢ ∀ (x2 : U × List U), seq_cons U (a1, l1) = seq_cons U x2 → (a1, l1) = x2
Tactic:
fix (a2, l2) : U × List U
State after:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
⊢ seq_cons U (a1, l1) = seq_cons U (a2, l2) → (a1, l1) = (a2, l2)

State before:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
⊢ seq_cons U (a1, l1) = seq_cons U (a2, l2) → (a1, l1) = (a2, l2)
Tactic:
assume h1 : seq_cons U (a1, l1) = seq_cons U (a2, l2)
State after:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : seq_cons U (a1, l1) = seq_cons U (a2, l2)
⊢ (a1, l1) = (a2, l2)

State before:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : seq_cons U (a1, l1) = seq_cons U (a2, l2)
⊢ (a1, l1) = (a2, l2)
Tactic:
rewrite [seq_cons_def, seq_cons_def] at h1
State after:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 :: l1 = a2 :: l2
⊢ (a1, l1) = (a2, l2)

State before:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 :: l1 = a2 :: l2
⊢ (a1, l1) = (a2, l2)
Tactic:
rewrite [List.cons_eq_cons] at h1
State after:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 = a2 ∧ l1 = l2
⊢ (a1, l1) = (a2, l2)

State before:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 = a2 ∧ l1 = l2
⊢ (a1, l1) = (a2, l2)
Tactic:
rewrite [h1.left, h1.right]
State after:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 = a2 ∧ l1 = l2
⊢ (a2, l2) = (a2, l2)

State before:
U : Type
a1 : U
l1 : List U
a2 : U
l2 : List U
h1 : a1 = a2 ∧ l1 = l2
⊢ (a2, l2) = (a2, l2)
Tactic:
rfl
State after:
no goals