-Lemma cheat1 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
- admit.
- Defined.
-Lemma cheat2 : forall {A}(t:list A), leaves (unleaves t) = t.
+Lemma updating_stripped_tree_is_inert'''' : forall Γ Δ ξ l tc atypes tbranches
+(x:StrongCaseBranchWithVVs(Γ:=Γ) VV eqd_vv tc atypes)
+(e0:Expr (sac_Γ x Γ) (sac_Δ x Γ atypes (weakCK'' Δ))
+ (scbwv_ξ x ξ l) (weakT' tbranches @@ weakL' l)) ,
+mapOptionTree (weakLT' ○ ξ)
+ (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
+unleaves (vec2list (sac_types x Γ atypes)) @@@ weakL' l
+=
+mapOptionTree (weakLT' ○ ξ)
+ (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
+ mapOptionTree
+ (update_ξ (weakLT' ○ ξ)
+ (vec2list
+ (vec_map
+ (fun
+ x0 : VV *
+ HaskType
+ (app (vec2list (sac_ekinds x)) Γ)
+ ★ => ⟨fst x0, snd x0 @@ weakL' l ⟩)
+ (vec_zip (scbwv_exprvars x)
+ (sac_types x Γ atypes)))))
+ (unleaves (vec2list (scbwv_exprvars x)))
+.