+let symmetric eq_ty l id uri m =
+ let eq = Cic.MutInd(uri,0,[]) in
+ let pred =
+ Cic.Lambda (Cic.Name "Sym",eq_ty,
+ Cic.Appl [CicSubstitution.lift 1 eq ;
+ CicSubstitution.lift 1 eq_ty;
+ Cic.Rel 1;CicSubstitution.lift 1 l])
+ in
+ let prefl =
+ Exact (Cic.Appl
+ [Cic.MutConstruct(uri,0,1,[]);eq_ty;l])
+ in
+ let id1 =
+ let eq = mk_equality (0,prefl,(eq_ty,l,l,Utils.Eq),m) in
+ let (_,_,_,_,id) = open_equality eq in
+ id
+ in
+ Step(Subst.empty_subst,
+ (Demodulation,id1,(Utils.Left,id),pred))
+;;
+