+ set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
+ (unleaves (vec2list (scbwv_exprvars (projT1 x))))
+ (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
+ _ _
+ ))) as q.
+
+rewrite cheat2 in q.
+rewrite cheat1.
+unfold weakCK'' in q.
+simpl in q.
+admit.
+(*
+replace (mapOptionTree ((@weakLT' Γ (tyConKind tc) _) ○ ξ)
+ (stripOutVars (vec2list (scbwv_exprvars (projT1 x)))
+ (expr2antecedent (projT2 x))))
+with (mapOptionTree (scbwv_ξ (projT1 x) ξ l)
+ (stripOutVars (vec2list (scbwv_exprvars (projT1 x)))
+ (expr2antecedent (projT2 x)))).
+rewrite <- cheat1 in q.
+rewrite vec2list_map_list2vec in q.
+unfold mapOptionTree.
+fold (@mapOptionTree (HaskType (app (tyConKind tc) Γ) ★)
+ (LeveledHaskType (app (tyConKind tc) Γ) ★) (fun t' => t' @@ weakL' l)).
+admit.
+*)
+admit.
+
+(*
+assert (
+
+unleaves (vec2list (vec_map (scbwv_ξ (projT1 x) ξ l) (scbwv_exprvars (projT1 x))))
+=
+unleaves (vec2list (sac_types (projT1 x) Γ atypes)) @@@ weakL'(κ:=tyConKind tc) l).
+admit.
+Set Printing Implicit.
+idtac.
+rewrite <- H.
+