fact: Definition gen_match_branch {T1 T2 X} (recursor : T1 -> M T2) (base : T2 -> M X) := fix f (C1_types C2_types : mlist Type) : forall ndc : (NDCfold (@iBase Typeₛ T1) C1_types), (lprod C2_types -> M X) -> M (branch_of_NDCTele (rsort := Propₛ) (it := @iBase Typeₛ T1) (fun _ => M X) (existT _ C1_types ndc)) := match C1_types as C1_types, C2_types as C2_types return forall ndc : (NDCfold (@iBase Typeₛ T1) C1_types), (lprod C2_types -> M X) -> M (branch_of_NDCTele (rsort := Propₛ) (it := @iBase Typeₛ T1) (fun _ => M X) (existT _ C1_types ndc)) with | mnil, mnil => fun (F1 : unit -> _) (F2 : unit -> _) => let c2 := reduce RedVmCompute (F2 tt) in M.ret c2 | X1:m:C1_types, X2:m:C2_types => mtmmatch (m: X1, X2) as Xs return forall ndc : (NDCfold (@iBase Typeₛ T1) (mfst Xs:m:C1_types)), (lprod (msnd Xs:m:C2_types) -> M X) -> M (branch_of_NDCTele (rsort := Propₛ) (it := @iBase Typeₛ T1) (fun _ => M X) (existT _ (mfst Xs:m:C1_types) ndc)) with | [? A : Type] (m: A, A) =u> fun (F1 : lprod (mfst (m: A,A):m:_) -> _) (F2 : lprod (msnd (m: A,A):m:_) -> M X)=> \fnuf a for F1, pat <- f C1_types C2_types (fun y=> F1 (m: a,y)) (fun lp => F2 (m: a,lp)); M.abs_fun (P:=fun _ => _) a pat | (m: T1, T2) =u> fun (F1 : lprod (mfst (m:T1,T2):m:_) -> _) (F2 : lprod (msnd (m:T1,T2):m:_) -> M X) => \fnuf a for F1, pat <- f C1_types C2_types (fun x=> F1 (m: a,x)) (fun lp => b <- recursor a; F2(m: b,lp)); M.abs_fun (P:=fun _ => _) a pat end | _, _ => fun _ _ => M.failwith "Constructors have different arity." end.
imports: Coq.Strings.String Mtac2(Base Logic Datatypes List Sorts DepDestruct MTeleMatch)