Bv quote fixitr

lemma bv_quote_fixitr (χ : _root_.LO.FirstOrder.Semiformula L ℕ 0) :    bv (V := ℕ) L (⌜(Rew.fixitr 0 χ.fvSup ▹ χ : _root_.LO.FirstOrder.Semiformula L ℕ (0 + χ.fvSup))⌝ : ℕ)      = χ.fvSup := by  -- the freevar-free closure body  have not_fvar_body : ∀ x, ¬(Rew.fixitr 0 χ.fvSup ▹ χ).FVar? x := by    intro x    rw [Rew.eq_bind (Rew.fixitr 0 χ.fvSup)]    simp only [Function.comp_def, Rew.fixitr_bvar, Rew.fixitr_fvar, Fin.natAdd_mk, zero_add]    intro hh    rcases Semiformula.fvar?_rew hh with (⟨z, hz⟩ | ⟨z, hz, hx⟩)    · simp at hz    · have : z < χ.fvSup := Semiformula.lt_fvSup_of_fvar? hz      simp [this] at hx  have hbsemi := Semiformula.quote_isSemiformula (V := ℕ)    (Rew.fixitr 0 χ.fvSup ▹ χ : _root_.LO.FirstOrder.Semiformula L ℕ (0 + χ.fvSup))  have hbU : IsUFormula L (⌜(Rew.fixitr 0 χ.fvSup ▹ χ : _root_.LO.FirstOrder.Semiformula L ℕ (0 + χ.fvSup))⌝ : ℕ) :=    hbsemi.isUFormula  -- `≤` direction: the body has `0 + fvSup` bound slots, so `bv ≤ fvSup` (model order over ℕ).  -- On ℕ the model cast is the identity (`natCast_nat`) and `<` is `Nat.lt`.  have hle := hbsemi.bv_le  simp only [Nat.zero_add, natCast_nat] at hle  -- the model `≤` on ℕ unfolds to `= ∨ <` with `<` the standard `Nat.lt`  rcases (hle : bv (V := ℕ) L (⌜(Rew.fixitr 0 χ.fvSup ▹ χ : _root_.LO.FirstOrder.Semiformula L ℕ (0 + χ.fvSup))⌝ : ℕ)      = χ.fvSup ∨ bv (V := ℕ) L (⌜(Rew.fixitr 0 χ.fvSup ▹ χ : _root_.LO.FirstOrder.Semiformula L ℕ (0 + χ.fvSup))⌝ : ℕ)      < χ.fvSup) with heq | hlt  · exact heq  -- `hlt : bv ⌜body⌝ < χ.fvSup` ; this case is impossible (forbids vacuous leading `∀`s)  exfalso  set j := bv (V := ℕ) L (⌜(Rew.fixitr 0 χ.fvSup ▹ χ : _root_.LO.FirstOrder.Semiformula L ℕ (0 + χ.fvSup))⌝ : ℕ) with hj  have hpos : 0 < χ.fvSup := by omega  have hsemi : IsSemiformula L j (⌜(Rew.fixitr 0 χ.fvSup ▹ χ : _root_.LO.FirstOrder.Semiformula L ℕ (0 + χ.fvSup))⌝ : ℕ) := by    have := IsUFormula.isSemiformula hbU; rwa [← hj] at this  obtain ⟨γ, hγ⟩ := IsSemiformula.sound hsemi  have hjle : j ≤ 0 + χ.fvSup := by omega  -- codes agree across levels, hence the formulas agree  have hcast : (Rew.castLE hjle ▹ γ : _root_.LO.FirstOrder.Semiformula L ℕ (0 + χ.fvSup))      = (Rew.fixitr 0 χ.fvSup ▹ χ : _root_.LO.FirstOrder.Semiformula L ℕ (0 + χ.fvSup)) := by    apply (Semiformula.quote_inj_iff (V := ℕ)).mp    rw [Semiformula.quote_castLE, hγ]  -- `γ` is free-variable-free  have hγfree : γ.freeVariables = ∅ := by    have hb : (Rew.fixitr 0 χ.fvSup ▹ χ : _root_.LO.FirstOrder.Semiformula L ℕ (0 + χ.fvSup)).freeVariables = ∅ :=      Finset.eq_empty_of_forall_notMem fun x hx ↦ not_fvar_body x hx    have := Semiformula.freeVariables_castLE γ hjle    rw [hcast, hb] at this; exact this.symm  -- invert the closure: `χ = γ ⇜ ![&0, …, &(j-1)]`  have hχeq : χ = γ ⇜ (fun i : Fin j ↦ (&↑i : SyntacticTerm L)) := by    have e1 : (Rew.fixitr 0 χ.fvSup ▹ χ : _root_.LO.FirstOrder.Semiformula L ℕ (0 + χ.fvSup))        ⇜ (fun x : Fin (0 + χ.fvSup) ↦ (&↑x : SyntacticTerm L)) = χ := Semiformula.subst_comp_fixitr χ    have hRewEq : (Rew.subst (fun x : Fin (0 + χ.fvSup) ↦ (&↑x : SyntacticTerm L))).comp (Rew.castLE hjle)        = Rew.subst (fun i : Fin j ↦ (&↑i : SyntacticTerm L)) := by      ext x <;> simp [Rew.comp_app]    symm    rw [← e1, ← hcast]    unfold Rewriting.subst    rw [← TransitiveRewriting.comp_app, hRewEq]  -- contradiction: `&(fvSup-1)` occurs in `χ`, but the inversion bounds free vars by `j ≤ fvSup-1`  have hfv : (γ ⇜ (fun i : Fin j ↦ (&↑i : SyntacticTerm L))).FVar? (χ.fvSup - 1) := by    rw [← hχeq]; exact Semiformula.fvar?_fvSup_pred χ hpos  unfold Rewriting.subst at hfv  rcases Semiformula.fvar?_rew hfv with (⟨i, hi⟩ | ⟨z, hz, _⟩)  · have hib : χ.fvSup - 1 = (i : ℕ) := by      simpa [Rew.subst_bvar, Semiterm.FVar?, Semiterm.freeVariables_fvar] using hi    have hij := i.isLt    omega  · simp [Semiformula.FVar?, hγfree] at hz