Ensures that let-in's in arities of inductive types work well. Maybe not

very useful in practice but as soon as let-in's were not forbidden in
the internal data structure, better to do it. Moreover, this gets
closer to the view were inductive definitions are uniformly built from
"contexts". (checker not changed!)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 182 insertions, 31 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 725859321c..8b2402bb54 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -135,6 +135,9 @@ type one_inductive_body = {
  (* Number of expected real arguments of the type (no let, no params) *)
     mind_nrealargs : int;
 
+ (* Length of realargs context (with let, no params) *)
+    mind_nrealargs_ctxt : int;
+
  (* List of allowed elimination sorts *)
     mind_kelim : sorts_family list;
 
@@ -223,6 +226,7 @@ let subst_mind_packet sub mbp =
     mind_arity = subst_arity sub mbp.mind_arity;
     mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
+    mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
     mind_kelim = mbp.mind_kelim;
     mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); 
     mind_nb_constant = mbp.mind_nb_constant;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index fb8317cdcb..454debd736 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -115,6 +115,9 @@ type one_inductive_body = {
  (* Number of expected real arguments of the type (no let, no params) *)
     mind_nrealargs : int;
 
+ (* Length of realargs context (with let, no params) *)
+    mind_nrealargs_ctxt : int;
+
  (* List of allowed elimination sorts *)
     mind_kelim : sorts_family list;
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4aac096fc4..ccf9b3f6c5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -588,6 +588,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
   (* Compute the set of used section variables *)
   let hyps =  used_section_variables env inds in
   let nparamargs = rel_context_nhyps params in
+  let nparamdecls = rel_context_length params in
   (* Check one inductive *)
   let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg =
     (* Type of constructors in normal form *)
@@ -629,6 +630,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
 	mind_arity = arkind;
 	mind_arity_ctxt = ar_sign;
 	mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
+	mind_nrealargs_ctxt = rel_context_length ar_sign - nparamdecls;
 	mind_kelim = kelim;
 	mind_consnames = Array.of_list cnames;
 	mind_consnrealdecls = consnrealargs;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 23cd99d1e9..6da102a940 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -270,16 +270,20 @@ let get_instantiated_arity (mib,mip) params =
 
 let elim_sorts (_,mip) = mip.mind_kelim
 
-let rel_list n m = 
-  let rec reln l p = 
-    if p>m then l else reln (mkRel(n+p)::l) (p+1)
+let extended_rel_list n hyps =
+  let rec reln l p = function
+    | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
+    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | [] -> l
   in 
-  reln [] 1
+  reln [] 1 hyps
 
 let build_dependent_inductive ind (_,mip) params =
-  let nrealargs = mip.mind_nrealargs in
+  let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
   applist 
-    (mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
+    (mkInd ind,
+       List.map (lift mip.mind_nrealargs_ctxt) params 
+       @ extended_rel_list 0 realargs)
 
 (* This exception is local *)
 exception LocalArity of (sorts_family * sorts_family * arity_error) option
@@ -309,6 +313,8 @@ let is_correct_arity env c pj ind specif params =
             with NotConvertible -> raise (LocalArity None) in
 	  check_allowed_sort ksort specif;
 	  Constraint.union u univ
+      | _, (_,Some _,_ as d)::ar' ->
+	  srec (push_rel d env) (lift 1 pt') ar' u
       | _ ->
 	  raise (LocalArity None)
   in 
@@ -339,8 +345,8 @@ let build_branches_type ind (_,mip as specif) params p =
 
 (* [p] is the predicate, [c] is the match object, [realargs] is the
    list of real args of the inductive type *)
-let build_case_type p c realargs =
-  beta_appvect p (Array.of_list (realargs@[c]))
+let build_case_type n p c realargs =
+  betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))
 
 let type_case_branches env (ind,largs) pj c =
   let specif = lookup_mind_specif env ind in 
@@ -349,7 +355,7 @@ let type_case_branches env (ind,largs) pj c =
   let p = pj.uj_val in
   let univ = is_correct_arity env c pj ind specif params in
   let lc = build_branches_type ind specif params p in
-  let ty = build_case_type p c realargs in
+  let ty = build_case_type (snd specif).mind_nrealargs_ctxt p c realargs in
   (lc, ty, univ)
 
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f1a44b5cac..89f1b443b9 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -117,6 +117,15 @@ let beta_appvect c v =
       | _ -> applist (substl env t, stack) in
   stacklam [] c (Array.to_list v)
 
+let betazeta_appvect n c v =
+  let rec stacklam n env t stack =
+    if n = 0 then applist (substl env t, stack) else
+    match kind_of_term t, stack with
+        Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+      | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack
+      | _ -> anomaly "Not enough lambda/let's" in
+  stacklam n [] c (Array.to_list v)
+
 (********************************************************************)
 (*                         Conversion                               *)
 (********************************************************************)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index de926bd1d6..9960513294 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -66,6 +66,9 @@ val default_conv_leq : types conversion_function
 (* Builds an application node, reducing beta redexes it may produce. *) 
 val beta_appvect : constr -> constr array -> constr
 
+(* Builds an application node, reducing the [n] first beta-zeta redexes. *) 
+val betazeta_appvect : int -> constr -> constr array -> constr
+
 (* Pseudo-reduction rule  Prod(x,A,B) a --> B[x\a] *)
 val hnf_prod_applist : env -> types -> constr list -> types
 
diff --git a/kernel/term.ml b/kernel/term.ml
index da8a778837..8a2c3278cb 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -26,7 +26,7 @@ type metavariable = int
 (* This defines Cases annotations *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
-  { ind_nargs : int; (* number of real args of the inductive type *)
+  { ind_nargs : int; (* length of the arity of the inductive type *)
     style     : case_style }
 type case_info =
   { ci_ind        : inductive;
diff --git a/kernel/term.mli b/kernel/term.mli
index 8f45e39f09..bc1cac44ae 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -42,7 +42,7 @@ type metavariable = int
 (*s Case annotation *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
-  { ind_nargs : int; (* number of real args of the inductive type *)
+  { ind_nargs : int; (* length of the arity of the inductive type *)
     style     : case_style }
 (* the integer is the number of real args, needed for reduction *)
 type case_info =
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 057f342aa6..1f9cc0f1f4 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -954,14 +954,18 @@ let adjust_impossible_cases pb pred tomatch submat =
 (* s.t Gamma,x1'..xn' |- match Pushed(x1')..Pushed(xn') rest with..end :pred'*)
 (*                                                                           *)
 (*****************************************************************************)
-let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
+let specialize_predicate newtomatchs (names,(depna,_)) arsign cs tms ccl =
   (* Assume some gamma st: gamma, (X,x:=realargs,copt), tms |- ccl *)
   let nrealargs = List.length names in
   let k = nrealargs + (if depna<>Anonymous then 1 else 0) in
   (* We adjust pred st: gamma, x1..xn, (X,x:=realargs,copt), tms |- ccl' *)
   let n = cs.cs_nargs in
   let ccl' = liftn_predicate n (k+1) ccl tms in
-  let argsi = if nrealargs <> 0 then Array.to_list cs.cs_concl_realargs else [] in
+  let argsi =
+    if nrealargs <> 0 then
+      adjust_subst_to_rel_context arsign (Array.to_list cs.cs_concl_realargs)
+    else
+      [] in
   let copti = if depna<>Anonymous then Some (build_dependent_constructor cs) else None in
   (* The substituends argsi, copti are all defined in gamma, x1...xn *)
   (* We need _parallel_ bindings to get gamma, x1...xn, tms |- ccl'' *)
@@ -1063,7 +1067,7 @@ let shift_problem ((current,t),_,(nadep,_)) pb =
      mat = List.map remove_current_pattern pb.mat }
 
 (* Building the sub-pattern-matching problem for a given branch *)
-let build_branch current deps (realnames,dep) pb eqns const_info =
+let build_branch current deps (realnames,dep) pb arsign eqns const_info =
   (* We remember that we descend through a constructor *)
   let alias_type =
     if Array.length const_info.cs_concl_realargs = 0
@@ -1120,7 +1124,7 @@ let build_branch current deps (realnames,dep) pb eqns const_info =
       1 typs' (List.rev dep_sign) in
 
   let pred = 
-    specialize_predicate typs'' (realnames,dep) const_info tomatch pb.pred in
+    specialize_predicate typs'' (realnames,dep) arsign const_info tomatch pb.pred in
 
   let currents = List.map (fun x -> Pushed x) typs'' in
 
@@ -1179,6 +1183,7 @@ and match_current pb tomatch =
     | IsInd (_,(IndType(indf,realargs) as indt),names) ->
 	let mind,_ = dest_ind_family indf in
 	let cstrs = get_constructors pb.env indf in
+	let arsign, _ = get_arity pb.env indf in
 	let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in
 	if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt  then
 	  compile (shift_problem ct pb)
@@ -1189,7 +1194,7 @@ and match_current pb tomatch =
 	  let pb = generalize_problem (names,dep) pb deps in
 
 	  (* We compile branches *)
-	  let brs = array_map2 (compile_branch current (names,dep) deps pb) eqns cstrs in
+	  let brs = array_map2 (compile_branch current (names,dep) deps pb arsign) eqns cstrs in
 
 	  (* We build the (elementary) case analysis *)
 	  let brvals = Array.map (fun (v,_) -> v) brs in
@@ -1202,8 +1207,8 @@ and match_current pb tomatch =
 	  { uj_val = applist (case, inst);
 	    uj_type = substl inst typ }
 
-and compile_branch current names deps pb eqn cstr =
-  let sign, pb = build_branch current deps names pb eqn cstr in
+and compile_branch current names deps pb arsign eqn cstr =
+  let sign, pb = build_branch current deps names pb arsign eqn cstr in
   let j = compile pb in
   (it_mkLambda_or_LetIn j.uj_val sign, j.uj_type)
 
@@ -1550,19 +1555,19 @@ let extract_arity_signature env0 tomatchl tmsign =
 	    str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = lift_inductive_family n indf in
-	  let (ind,params) = dest_ind_family indf' in
-	  let nrealargs = List.length realargs in
+	  let (ind,_) = dest_ind_family indf' in
+	  let nparams_ctxt,nrealargs_ctxt = inductive_nargs env0 ind in
+	  let arsign = fst (get_arity env0 indf') in
 	  let realnal =
 	    match t with
 	      | Some (loc,ind',nparams,realnal) ->
 		  if ind <> ind' then
 		    user_err_loc (loc,"",str "Wrong inductive type.");
-		  if List.length params <> nparams
-		    or nrealargs <> List.length realnal then
+		  if nparams_ctxt <> nparams
+		    or nrealargs_ctxt <> List.length realnal then
 		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
-	      | None -> list_make nrealargs Anonymous in
-	  let arsign = fst (get_arity env0 indf') in
+	      | None -> list_make nrealargs_ctxt Anonymous in
 (* 	  let na =  *)
 (* 	    match na with  *)
 (* 	      | Name _ -> na *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 6a4c066ce5..0b07bc8599 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -58,7 +58,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
       (RecursionSchemeError
 	 (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind)));
 
-  let ndepar = mip.mind_nrealargs + 1 in
+  let ndepar = mip.mind_nrealargs_ctxt + 1 in
 
   (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
   (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
@@ -594,3 +594,56 @@ let lookup_eliminator ind_sp s =
        pr_global_env Idset.empty (IndRef ind_sp) ++ 
        strbrk " on sort " ++ pr_sort_family s ++
        strbrk " is probably not allowed.")
+
+(* Build the congruence lemma associated to an inductive type 
+   I p1..pn a1..am with one constructor C : I q1..qn b1..bm *)
+
+(* TODO: extend it to types with more than one index *)
+
+let build_congr env (eq,refl) ind (mib,mip) =
+  if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
+    error "Not an inductive type with a single constructor.";
+  if mip.mind_nrealargs <> 1 then
+    error "Expect an inductive type with one predicate parameter.";
+  let i = 1 in
+  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  if List.exists (fun (_,b,_) -> b <> None) realsign then
+    error "Inductive equalities with local definitions in arity not supported";
+  let env_with_arity = push_rel_context mip.mind_arity_ctxt env in
+  let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
+  let _,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+  let _,constrargs = decompose_app ccl in
+  let c = List.nth constrargs (i - 1) in
+  let varB = id_of_string "B" in
+  let varH = id_of_string "H" in
+  let varf = id_of_string "f" in
+  let ci = make_case_info (Global.env()) ind RegularStyle in
+  let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn ~init:c s in
+  let my_it_mkLambda_or_LetIn_name s c = it_mkLambda_or_LetIn_name env c s in
+  my_it_mkLambda_or_LetIn mib.mind_params_ctxt
+     (mkNamedLambda varB (new_Type ())
+     (mkNamedLambda varf (mkArrow (lift 1 ty) (mkVar varB))
+     (my_it_mkLambda_or_LetIn_name (lift_rel_context 2 realsign)
+     (mkNamedLambda varH
+        (applist
+           (mkInd ind,
+	    extended_rel_list (mip.mind_nrealargs+2) mib.mind_params_ctxt @
+	    extended_rel_list 0 realsign))
+     (mkCase (ci,
+       my_it_mkLambda_or_LetIn_name
+	 (lift_rel_context (mip.mind_nrealargs+3) realsign)
+         (mkLambda
+           (Anonymous,
+            applist
+             (mkInd ind,
+	        extended_rel_list (2*mip.mind_nrealargs+3) mib.mind_params_ctxt
+	        @ extended_rel_list 0 realsign),
+            mkApp (eq, 
+	      [|mkVar varB;
+                mkApp (mkVar varf, [|lift (2*mip.mind_nrealargs+3) c|]);
+		mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))),
+       mkVar varH,
+       [|mkApp (refl,
+          [|mkVar varB;
+	    mkApp (mkVar varf, [|lift (mip.mind_nrealargs+2) c|])|])|]))))))
+ 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 45fbe3227b..3150ed63b5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -129,7 +129,7 @@ let get_full_arity_sign env ind =
 
 let inductive_nargs env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  mib.mind_nparams, mip.mind_nrealargs
+  (rel_context_length (mib.mind_params_ctxt), mip.mind_nrealargs_ctxt)
 
 let allowed_sorts env (kn,i as ind) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -138,7 +138,7 @@ let allowed_sorts env (kn,i as ind) =
 (* Annotation for cases *)
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let print_info = { ind_nargs = mip.mind_nrealargs; style = style } in
+  let print_info = { ind_nargs = mip.mind_nrealargs_ctxt; style = style } in
   { ci_ind     = ind;
     ci_npar    = mib.mind_nparams;
     ci_cstr_nargs = mip.mind_consnrealdecls;
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 357fb09082..cc1bb7f418 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -58,7 +58,7 @@ val mis_nf_constructor_type :
 val mis_constr_nargs : inductive -> int array
 val mis_constr_nargs_env : env -> inductive -> int array
 
-(* Return number of expected parameters and of expected real arguments *)
+(* Return the lengths of parameters signature and real arguments signature *)
 val inductive_nargs : env -> inductive -> int * int
 
 val mis_constructor_nargs_env : env -> constructor -> int
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 4034d86674..47bc972513 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -1096,6 +1096,25 @@ let substl_rel_context l =
 let lift_rel_context n =
   map_rel_context_with_binders (liftn n)
 
+let smash_rel_context sign =
+  let rec aux acc = function
+  | [] -> acc
+  | (_,None,_ as d) :: l -> aux (d::acc) l
+  | (_,Some b,_) :: l ->
+      (* Quadratic in the number of let but there are probably a few of them *)
+      aux (List.rev (substl_rel_context [b] (List.rev acc))) l
+  in List.rev (aux [] sign)
+
+let adjust_subst_to_rel_context sign l =
+  let rec aux subst sign l =
+    match sign, l with 
+    | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args'
+    | (_,Some c,_)::sign', args' ->
+	aux (substl (List.rev subst) c :: subst) sign' args'
+    | [], [] -> List.rev subst
+    | _ -> anomaly "Instance and signature do not match"
+  in aux [] (List.rev sign) l
+
 let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init
 
 let rec mem_named_context id = function
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index f9d4329077..3d167ebb03 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -267,6 +267,8 @@ val process_rel_context : (rel_declaration -> env -> env) -> env -> env
 val assums_of_rel_context : rel_context -> (name * constr) list
 val lift_rel_context : int -> rel_context -> rel_context
 val substl_rel_context : constr list -> rel_context -> rel_context
+val smash_rel_context : rel_context -> rel_context (* expand lets in context *)
+val adjust_subst_to_rel_context : rel_context -> constr list -> constr list
 val map_rel_context_in_env :
   (env -> constr -> constr) -> env -> rel_context -> rel_context
 val map_rel_context_with_binders : 
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 1adcbd39a1..724ba502c7 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -1,4 +1,32 @@
-(* Check local definitions in context of inductive types *)
+(* Test des definitions inductives imbriquees *)
+
+Require Import List.
+
+Inductive X : Set :=
+    cons1 : list X -> X.
+
+Inductive Y : Set :=
+    cons2 : list (Y * Y) -> Y.
+
+(* Test inductive types with local definitions (arity) *)
+
+Inductive eq1 : forall A:Type, let B:=A in A -> Prop :=
+  refl1 : eq1 True I.
+
+Check 
+ fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) =>
+   let B := A in
+     fun (a : A) (e : eq1 A a) =>
+       match e in (eq1 A0 B0 a0) return (P A0 a0) with
+       | refl1 => f
+       end.
+
+Inductive eq2 (A:Type) (a:A)
+  : forall B C:Type, let D:=(A*B*C)%type in D -> Prop :=
+  refl2 : eq2 A a unit bool (a,tt,true).
+
+(* Check inductive types with local definitions (parameters) *)
+
 Inductive A (C D : Prop) (E:=C) (F:=D) (x y : E -> F) : E -> Set :=
     I : forall z : E, A C D x y z.
 
@@ -9,7 +37,7 @@ Check
    fun (x y : E -> F) (P : forall c : C, A C D x y c -> Type)
      (f : forall z : C, P z (I C D x y z)) (y0 : C) 
      (a : A C D x y y0) =>
-   match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with
+   match a as a0 in (A _ _ _ _ _ _ y1) return (P y1 a0) with
    | I x0 => f x0
    end).
 
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 2aec6e9b1c..1cf707583b 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -5,7 +5,8 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* Teste des definitions inductives imbriquees *)
+
+(* Test des definitions inductives imbriquees *)
 
 Require Import List.
 
@@ -15,3 +16,19 @@ Inductive X : Set :=
 Inductive Y : Set :=
     cons2 : list (Y * Y) -> Y.
 
+(* Test inductive types with local definitions *)
+
+Inductive eq1 : forall A:Type, let B:=A in A -> Prop :=
+  refl1 : eq1 True I.
+
+Check 
+ fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) =>
+   let B := A in
+     fun (a : A) (e : eq1 A a) =>
+       match e in (eq1 A0 B0 a0) return (P A0 a0) with
+       | refl1 => f
+       end.
+
+Inductive eq2 (A:Type) (a:A)
+  : forall B C:Type, let D:=(A*B*C)%type in D -> Prop :=
+  refl2 : eq2 A a unit bool (a,tt,true).