Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} :=
{ scbwv_exprvars : vec VV (sac_numExprVars sac)
; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars)
Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} :=
{ scbwv_exprvars : vec VV (sac_numExprVars sac)
; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars)