fact: Definition branch_map {A} {B} (y : A) (g : (goal _)) (b : branch A (fun a => gtactic (B a))) : branch A (fun y => M (mlist (B y *m (goal _)))) := match b in branch A' P' return forall B : A' -> Type, forall P_eq : P' =m= fun a => gtactic (B a), branch A' (fun y => M (mlist (B y *m (goal _)))) with | @branch_pattern _ _ p => fun B P_eq => let op p := branch_pattern (pattern_map g p) in ltac:(rewrite P_eq in p; refine (op p)) | branch_app_static U ct cont => fun _ P_eq => let cont := ltac:(rewrite P_eq in cont; refine cont) in let cont := MTele.MTele_constmap_app (si:=Typeₛ) Propₛ (fun _ _ => _) ct cont g in @branch_app_static _ _ _ U _ cont | branch_forallP cont => fun _ P_eq => let cont := ltac:(rewrite P_eq in cont; refine cont) in branch_forallP (fun x y => cont x y g) | branch_forallT cont => fun _ P_eq => let cont := ltac:(rewrite P_eq in cont; refine cont) in branch_forallT (fun x y => cont x y g) end B meq_refl.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic intf.Sorts) Strings.String NArith.BinNat NArith.BinNatDef