+
+
+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)))
+.
+admit.
+Qed.
+
+
+