- mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
- -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
- -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
- { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
+ mapOptionTreeAndFlatten (fun x => snd x) alts = mapOptionTree ξ vars
+ -> ITree Judg judg2exprType (mapOptionTree (fun x => @pcb_judg tc Γ Δ lev avars tbranches (fst x) (snd x)) alts)
+ -> ITree _ (fun q => prod (judg2exprType (@pcb_judg tc Γ Δ lev avars tbranches (fst q) (snd q)))
+ { vars' : _ & (snd q) = mapOptionTree ξ vars' })