- { scbwv_sac : @StrongAltCon tc
- ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac)
- ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes)
- ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (vec2list
- (vec_map (fun x => ((fst x),(snd x @@ weakL' lev))) scbwv_varstypes))
+ { scbwv_sac : @StrongAltCon tc
+ ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac)
+ ; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars)
+ ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes)
+ ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes)