[GOAL]
α : Type u
n : ℕ
f : Fin n → α
⊢ length (ofFn f) = n
[PROOFSTEP]
simp [ofFn]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
⊢ length (ofFn f) = n
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
⊢ get (ofFn f) i = f (↑(Fin.castIso (_ : length (ofFn f) = n)) i)
[PROOFSTEP]
have := Array.getElem_ofFn f i (by simpa using i.2)
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
⊢ ↑i < Array.size (Array.ofFn f)
[PROOFSTEP]
simpa using i.2
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
this : (Array.ofFn f)[↑i] = f { val := ↑i, isLt := (_ : ↑i < n) }
⊢ get (ofFn f) i = f (↑(Fin.castIso (_ : length (ofFn f) = n)) i)
[PROOFSTEP]
cases' i with i hi
[GOAL]
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  (Array.ofFn f)[↑{ val := i, isLt := hi }] =
    f { val := ↑{ val := i, isLt := hi }, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f (↑(Fin.castIso (_ : length (ofFn f) = n)) { val := i, isLt := hi })
[PROOFSTEP]
simp only [getElem, Array.get] at this 
[GOAL]
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f (↑(Fin.castIso (_ : length (ofFn f) = n)) { val := i, isLt := hi })
[PROOFSTEP]
simp only [Fin.castIso_mk]
[GOAL]
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f { val := i, isLt := (_ : i < n) }
[PROOFSTEP]
rw [← this]
[GOAL]
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } =
    get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }
[PROOFSTEP]
congr
[GOAL]
case mk.h.e_2.h
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ ofFn f = (Array.ofFn f).data
[PROOFSTEP]
simp [ofFn]
[GOAL]
case mk.h.e_3.e_1.e_a
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ ofFn f = (Array.ofFn f).data
[PROOFSTEP]
simp [ofFn]
[GOAL]
case mk.h.e_3.e_3
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ HEq hi (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f))
[PROOFSTEP]
simp [ofFn]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : i < length (ofFn f)
⊢ get? (ofFn f) i = ofFnNthVal f i
[PROOFSTEP]
rw [get?_eq_get h, get_ofFn]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : i < length (ofFn f)
⊢ some (f (↑(Fin.castIso (_ : length (ofFn f) = n)) { val := i, isLt := h })) = ofFnNthVal f i
[PROOFSTEP]
simp at h 
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h✝ : i < length (ofFn f)
h : i < n
⊢ some (f (↑(Fin.castIso (_ : length (ofFn f) = n)) { val := i, isLt := h✝ })) = ofFnNthVal f i
[PROOFSTEP]
simp [ofFnNthVal, h]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : ¬i < length (ofFn f)
⊢ get? (ofFn f) i = ofFnNthVal f i
[PROOFSTEP]
rw [ofFnNthVal, dif_neg]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : ¬i < length (ofFn f)
⊢ get? (ofFn f) i = none
[PROOFSTEP]
simpa using h
[GOAL]
case hnc
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
h : ¬i < length (ofFn f)
⊢ ¬i < n
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
i : Fin n
⊢ nthLe (ofFn f) ↑i (_ : ↑i < length (ofFn f)) = f i
[PROOFSTEP]
simp [nthLe]
[GOAL]
α : Type u
β : Type u_1
n : ℕ
f : Fin n → α
g : α → β
⊢ length (map g (ofFn f)) = length (ofFn (g ∘ f))
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type u_1
n : ℕ
f : Fin n → α
g : α → β
i : ℕ
h : i < length (map g (ofFn f))
h' : i < length (ofFn (g ∘ f))
⊢ get (map g (ofFn f)) { val := i, isLt := h } = get (ofFn (g ∘ f)) { val := i, isLt := h' }
[PROOFSTEP]
simp
[GOAL]
α : Type u
m n : ℕ
h : m = n
f : Fin m → α
⊢ ofFn f = ofFn fun i => f (↑(Fin.castIso (_ : n = m)) i)
[PROOFSTEP]
subst h
[GOAL]
α : Type u
m : ℕ
f : Fin m → α
⊢ ofFn f = ofFn fun i => f (↑(Fin.castIso (_ : m = m)) i)
[PROOFSTEP]
simp_rw [Fin.castIso_refl, OrderIso.refl_apply]
[GOAL]
α : Type u
n : ℕ
f : Fin (succ n) → α
⊢ length (ofFn f) = length (f 0 :: ofFn fun i => f (Fin.succ i))
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
f : Fin (succ n) → α
i : ℕ
hi₁ : i < length (ofFn f)
hi₂ : i < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := i, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := i, isLt := hi₂ }
[PROOFSTEP]
cases i
[GOAL]
case zero
α : Type u
n : ℕ
f : Fin (succ n) → α
hi₁ : zero < length (ofFn f)
hi₂ : zero < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := zero, isLt := hi₁ } = get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := zero, isLt := hi₂ }
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u
n : ℕ
f : Fin (succ n) → α
n✝ : ℕ
hi₁ : succ n✝ < length (ofFn f)
hi₂ : succ n✝ < length (f 0 :: ofFn fun i => f (Fin.succ i))
⊢ get (ofFn f) { val := succ n✝, isLt := hi₁ } =
    get (f 0 :: ofFn fun i => f (Fin.succ i)) { val := succ n✝, isLt := hi₂ }
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
f : Fin (succ n) → α
⊢ ofFn f = concat (ofFn fun i => f (Fin.castSucc i)) (f (Fin.last n))
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
α : Type u
n : ℕ
f✝ : Fin (succ n) → α
f : Fin (succ zero) → α
⊢ ofFn f = concat (ofFn fun i => f (Fin.castSucc i)) (f (Fin.last zero))
[PROOFSTEP]
rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero]
[GOAL]
case zero
α : Type u
n : ℕ
f✝ : Fin (succ n) → α
f : Fin (succ zero) → α
⊢ [f 0] = [f (Fin.last zero)]
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
n✝ : ℕ
f✝ : Fin (succ n✝) → α
n : ℕ
IH : ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (Fin.castSucc i)) (f (Fin.last n))
f : Fin (succ (succ n)) → α
⊢ ofFn f = concat (ofFn fun i => f (Fin.castSucc i)) (f (Fin.last (succ n)))
[PROOFSTEP]
rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero]
[GOAL]
case succ
α : Type u
n✝ : ℕ
f✝ : Fin (succ n✝) → α
n : ℕ
IH : ∀ (f : Fin (succ n) → α), ofFn f = concat (ofFn fun i => f (Fin.castSucc i)) (f (Fin.last n))
f : Fin (succ (succ n)) → α
⊢ f 0 :: concat (ofFn fun i => f (Fin.succ (Fin.castSucc i))) (f (Fin.succ (Fin.last n))) =
    f 0 :: concat (ofFn fun i => f (Fin.castSucc (Fin.succ i))) (f (Fin.last (succ n)))
[PROOFSTEP]
congr
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
⊢ ofFn f = [] ↔ n = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u
f : Fin zero → α
⊢ ofFn f = [] ↔ zero = 0
[PROOFSTEP]
simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero]
[GOAL]
case succ
α : Type u
n✝ : ℕ
f : Fin (succ n✝) → α
⊢ ofFn f = [] ↔ succ n✝ = 0
[PROOFSTEP]
simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
h : ofFn f ≠ []
hn : optParam (n - 1 < n) (_ : pred (Nat.sub n 0) < Nat.sub n 0)
⊢ getLast (ofFn f) h = f { val := n - 1, isLt := hn }
[PROOFSTEP]
simp [getLast_eq_get]
[GOAL]
α : Type u
m n : ℕ
f : Fin (m + n) → α
⊢ ofFn f = (ofFn fun i => f (Fin.castAdd n i)) ++ ofFn fun j => f (Fin.natAdd m j)
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
α : Type u
m n : ℕ
f✝ : Fin (m + n) → α
f : Fin (m + zero) → α
⊢ ofFn f = (ofFn fun i => f (Fin.castAdd zero i)) ++ ofFn fun j => f (Fin.natAdd m j)
[PROOFSTEP]
rw [ofFn_zero, append_nil, Fin.castAdd_zero]
[GOAL]
case zero
α : Type u
m n : ℕ
f✝ : Fin (m + n) → α
f : Fin (m + zero) → α
⊢ ofFn f = ofFn fun i => f (Fin.cast (_ : m = m) i)
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u
m n✝ : ℕ
f✝ : Fin (m + n✝) → α
n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (Fin.castAdd n i)) ++ ofFn fun j => f (Fin.natAdd m j)
f : Fin (m + succ n) → α
⊢ ofFn f = (ofFn fun i => f (Fin.castAdd (succ n) i)) ++ ofFn fun j => f (Fin.natAdd m j)
[PROOFSTEP]
rw [ofFn_succ', ofFn_succ', IH, append_concat]
[GOAL]
case succ
α : Type u
m n✝ : ℕ
f✝ : Fin (m + n✝) → α
n : ℕ
IH : ∀ (f : Fin (m + n) → α), ofFn f = (ofFn fun i => f (Fin.castAdd n i)) ++ ofFn fun j => f (Fin.natAdd m j)
f : Fin (m + succ n) → α
⊢ concat ((ofFn fun i => f (Fin.castSucc (Fin.castAdd n i))) ++ ofFn fun j => f (Fin.castSucc (Fin.natAdd m j)))
      (f (Fin.last (Nat.add m n))) =
    concat ((ofFn fun i => f (Fin.castAdd (succ n) i)) ++ ofFn fun i => f (Fin.natAdd m (Fin.castSucc i)))
      (f (Fin.natAdd m (Fin.last n)))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ofFn (Fin.append a b) = ofFn a ++ ofFn b
[PROOFSTEP]
simp_rw [ofFn_add, Fin.append_left, Fin.append_right]
[GOAL]
α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })
[PROOFSTEP]
induction' m with m IH
[GOAL]
case zero
α : Type u
m n : ℕ
f✝ : Fin (m * n) → α
f : Fin (zero * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < zero * n) })
[PROOFSTEP]
simp [ofFn_zero, zero_mul, ofFn_zero, join]
[GOAL]
case succ
α : Type u
m✝ n : ℕ
f✝ : Fin (m✝ * n) → α
m : ℕ
IH :
  ∀ (f : Fin (m * n) → α),
    ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })
f : Fin (succ m * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
[PROOFSTEP]
simp_rw [ofFn_succ', succ_mul, join_concat, ofFn_add, IH]
[GOAL]
case succ
α : Type u
m✝ n : ℕ
f✝ : Fin (m✝ * n) → α
m : ℕ
IH :
  ∀ (f : Fin (m * n) → α),
    ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })
f : Fin (succ m * n) → α
⊢ (join
        (ofFn fun i =>
          ofFn fun j =>
            f
              (↑(Fin.castIso (_ : m * n + n = succ m * n))
                (Fin.castAdd n { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) }))) ++
      ofFn fun j => f (↑(Fin.castIso (_ : m * n + n = succ m * n)) (Fin.natAdd (m * n) j))) =
    join
        (ofFn fun i =>
          ofFn fun j =>
            f { val := ↑(Fin.castSucc i) * n + ↑j, isLt := (_ : ↑(Fin.castSucc i) * n + ↑j < succ m * n) }) ++
      ofFn fun j => f { val := ↑(Fin.last m) * n + ↑j, isLt := (_ : ↑(Fin.last m) * n + ↑j < succ m * n) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := m * ↑i + ↑j, isLt := (_ : m * ↑i + ↑j < m * n) })
[PROOFSTEP]
simp_rw [mul_comm m n, mul_comm m, ofFn_mul, Fin.castIso_mk]
[GOAL]
α : Type u
a : α
l : List α
⊢ ofFn (get (a :: l)) = a :: l
[PROOFSTEP]
rw [ofFn_succ]
[GOAL]
α : Type u
a : α
l : List α
⊢ (get (a :: l) 0 :: ofFn fun i => get (a :: l) (Fin.succ i)) = a :: l
[PROOFSTEP]
congr
[GOAL]
case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i => get (a :: l) (Fin.succ i)) = l
[PROOFSTEP]
exact ofFn_get l
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ a ∈ Set.range f
[PROOFSTEP]
simp only [mem_iff_get, Set.mem_range, get_ofFn]
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ (∃ n_1, f (↑(Fin.castIso (_ : length (ofFn f) = n)) n_1) = a) ↔ ∃ y, f y = a
[PROOFSTEP]
exact ⟨fun ⟨i, hi⟩ => ⟨Fin.castIso (by simp) i, hi⟩, fun ⟨i, hi⟩ => ⟨Fin.castIso (by simp) i, hi⟩⟩
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
a : α
x✝ : ∃ n_1, f (↑(Fin.castIso (_ : length (ofFn f) = n)) n_1) = a
i : Fin (length (ofFn f))
hi : f (↑(Fin.castIso (_ : length (ofFn f) = n)) i) = a
⊢ length (ofFn f) = n
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
a : α
x✝ : ∃ y, f y = a
i : Fin n
hi : f i = a
⊢ n = length (ofFn f)
[PROOFSTEP]
simp
[GOAL]
α : Type u
n : ℕ
f : Fin n → α
P : α → Prop
⊢ (∀ (i : α), i ∈ ofFn f → P i) ↔ ∀ (j : Fin n), P (f j)
[PROOFSTEP]
simp only [mem_ofFn, Set.forall_range_iff]
[GOAL]
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x => c) = replicate (n + 1) c
[PROOFSTEP]
rw [replicate, ← ofFn_const n]
[GOAL]
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x => c) = c :: ofFn fun x => c
[PROOFSTEP]
simp
[GOAL]
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ ofFn (Fin.repeat n a) = join (replicate n (ofFn a))
[PROOFSTEP]
simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, add_comm, Nat.add_mul_mod_self_right,
  Nat.mod_eq_of_lt (Fin.is_lt _)]
[GOAL]
α : Type u
R : α → α → Prop
n : ℕ
f : Fin n → α
⊢ Pairwise R (ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)
[PROOFSTEP]
simp only [pairwise_iff_get, (Fin.castIso (length_ofFn f)).surjective.forall, get_ofFn, OrderIso.lt_iff_lt]
[GOAL]
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
⊢ ofFnRec h (ofFn f) = h n f
[PROOFSTEP]
have := (@equivSigmaTuple α).rightInverse_symm
[GOAL]
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this : Function.RightInverse ↑equivSigmaTuple.symm ↑equivSigmaTuple
⊢ ofFnRec h (ofFn f) = h n f
[PROOFSTEP]
dsimp [equivSigmaTuple] at this 
[GOAL]
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
⊢ ofFnRec h (ofFn f) = h n f
[PROOFSTEP]
have := this.cast_eq (fun s => h s.1 s.2) ⟨n, f⟩
[GOAL]
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this✝ : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
this :
  cast
      (_ :
        C (ofFn { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.snd) =
          C (ofFn { fst := n, snd := f }.snd))
      (h { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.fst
        { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.snd) =
    h { fst := n, snd := f }.fst { fst := n, snd := f }.snd
⊢ ofFnRec h (ofFn f) = h n f
[PROOFSTEP]
dsimp only at this 
[GOAL]
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this✝ : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
this :
  cast (_ : C (ofFn { fst := length (ofFn f), snd := get (ofFn f) }.snd) = C (ofFn { fst := n, snd := f }.snd))
      (h (length (ofFn f)) (get (ofFn f))) =
    h n f
⊢ ofFnRec h (ofFn f) = h n f
[PROOFSTEP]
rw [ofFnRec, ← this]
[GOAL]
α : Type u
n : ℕ
f g : Fin n → α
h : ofFn f = ofFn g
⊢ HEq f g
[PROOFSTEP]
rw [ofFn_inj'] at h 
[GOAL]
α : Type u
n : ℕ
f g : Fin n → α
h : { fst := n, snd := f } = { fst := n, snd := g }
⊢ HEq f g
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Type u
n : ℕ
f : Fin n → α
⊢ HEq f f
[PROOFSTEP]
rfl
