Add more instances for type.related

1 files changed, 15 insertions, 4 deletions

diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index 6c90d4ecc..9393a1ebf 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -38,17 +38,28 @@ Module Compilers.
       Context {base_type} {interp_base_type : base_type -> Type}.
       Local Notation eqv := (@type.related base_type interp_base_type (fun _ => eq)).
 
-      Global Instance eqv_Symmetric {t} : Symmetric (@eqv t) | 10.
-      Proof. induction t; cbn [type.eqv type.interp] in *; repeat intro; eauto. Qed.
+      Global Instance related_Symmetric {t} {R : forall t, relation (interp_base_type t)}
+             {R_sym : forall t, Symmetric (R t)}
+        : Symmetric (@type.related base_type interp_base_type R t) | 10.
+      Proof.
+        cbv [Symmetric] in *;
+          induction t; cbn [type.related type.interp] in *; repeat intro; eauto.
+      Qed.
 
-      Global Instance eqv_Transitive {t} : Transitive (@eqv t) | 10.
+      Global Instance related_Transitive {t} {R : forall t, relation (interp_base_type t)}
+             {R_sym : forall t, Symmetric (R t)}
+             {R_trans : forall t, Transitive (R t)}
+        : Transitive (@type.related base_type interp_base_type R t) | 10.
       Proof.
-        induction t; cbn [eqv]; [ exact _ | ].
+        induction t; cbn [type.related]; [ exact _ | ].
         cbv [respectful]; cbn [type.interp].
         intros f g h Hfg Hgh x y Hxy.
         etransitivity; [ eapply Hfg; eassumption | eapply Hgh ].
         etransitivity; first [ eassumption | symmetry; eassumption ].
       Qed.
+
+      Global Instance eqv_Transitive {t} : Transitive (@eqv t) | 10 := _.
+      Global Instance eqv_Symmetric {t} : Symmetric (@eqv t) | 10 := _.
     End eqv.
 
     Section app_curried_instances.