LEGO Version 1.3: Elimination Rule for Relations

  Inductive [R:T1->..->Tn->UNIV] Relation
  Constructors
    [rule1 : {x1:t1}..{xk:tk} (* schematic variables *)

                (* inductive premises *)
            (R p1 .. pn)->..->(R p'1 .. p'n)->       (* side conditions *)
        (*--------------------------------------*) S1->..->Sn->
                     R c1 .. cn
                  (* conclusion *)                               ]
    (* more rules *)
    [ruleN: (* same pattern *) ];

Previously, the elimination rule generated and assumed was

  R_elim : {C_R:T1->..->Tn->UNIV} (* C_R does not depend on proofs of R *)
              ({x1:t1}..{xk:tk}S1->..->Sn-> (* rule1 case *)
               (C_R p1 .. pn)->..->(C_R p'1 .. p'n)->C_R c1 .. cn)->
              (* more cases *)
                   {a1:T1}..{an:Tn}(R a1 .. an)->C_R a1 .. an

This captured directly the idea that R is the smallest relation satisfying its rules.

However, observe that in each case, we get (C_R p1 .. pn) etc as hypotheses, but not the (R p1 .. pn) etc themselves, often very useful. We can add these hypotheses for a given

  C_R = [b1:T1]..[bn:Tn]P

by replacing it with

  C_R = [b1:T1]..[bn:Tn]and (R b1 .. bn) P

and reconstructing explicitly the proof of (R b1 .. bn) we morally already have.

In the light of this, and since it is easier to ignore useless hypotheses than to reconstruct useful ones, we now add them in when we generate the elimination rule, which now looks like this:

  R_elim : {C_R:T1->..->Tn->UNIV} (* C_R does not depend on proofs of R *)
              ({x1:t1}..{xk:tk}S1->..->Sn-> (* rule1 case *)
               (R p1 .. pn)->..->(R p'1 .. p'n)->
               (C_R p1 .. pn)->..->(C_R p'1 .. p'n)->C_R c1 .. cn)->
              (* more cases *)
                   {a1:T1}..{an:Tn}(R a1 .. an)->C_R a1 .. an

This formulation is no stronger than the previous one, but hopefully more convenient.