-Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts',
- mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
- = ((mapOptionTreeAndFlatten pcb_freevars (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)).
+
+Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
+ (alts':Tree
+ ??{sac : StrongAltCon &
+ {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
+ Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ))
+ (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))}}),
+
+ (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
+ (mapOptionTree mkProofCaseBranch alts'))
+ ,,
+ mapOptionTree ξ (expr2antecedent e) =
+ mapOptionTree ξ
+ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).