-Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
-(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
- & Expr (sac_gamma sac Γ)
- (sac_delta sac Γ atypes (weakCK'' Δ))
- (scbwv_xi scb ξ l)
- (weakT' tbranches) (weakL' l) } })
- : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
- destruct alt.
- exists x.
- exact
- {| pcb_freevars := mapOptionTree ξ
- (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
- (expr2antecedent (projT2 s)))
- |}.
- Defined.
-
-