- match body,pos with
-(*
- |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let uri_sym = LibraryObjects.sym_eq_URI ~eq in
- mk_trans uri_trans ty other what third
- (mk_sym uri_sym ty what other p2) p1
- |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- mk_trans uri_trans ty other what third p2 p1
- |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- mk_trans uri_trans ty third what other p1 p2
- |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let uri_sym = LibraryObjects.sym_eq_URI ~eq in
- mk_trans uri_trans ty third what other p1
- (mk_sym uri_sym ty other what p2)
- | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs
- ->
- let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t lhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
- (inject ty lhs m r pmr) (inject ty lhs l m plm)
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2)
- in
- mk_trans uri_trans ty pred_of_other pred_of_what rhs
- (inject ty lhs what other p2) p1
- | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
- ->
- let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t lhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
- (inject ty lhs m l plm)
- (inject ty lhs r m pmr)
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other =
- CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- mk_eq_ind (Utils.eq_ind_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2
- in
- mk_trans uri_trans ty pred_of_other pred_of_what rhs
- (inject ty lhs what other p2) p1
- | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
- ->
- let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t rhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
- (inject ty lhs m r pmr)
- (inject ty lhs l m plm)
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2)
- in
- mk_trans uri_trans ty lhs pred_of_what pred_of_other
- p1 (inject ty rhs other what p2)
- | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
- ->
- let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t rhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
- (inject ty lhs m l plm)
- (inject ty lhs r m pmr))
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- mk_eq_ind (Utils.eq_ind_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2
- in
- mk_trans uri_trans ty lhs pred_of_what pred_of_other
- p1 (inject ty rhs other what p2)
-*)
- | _, Utils.Left ->
- mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
- | _, Utils.Right ->
- mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2