(s : Sort σ) (x : (A&&P) s) (y : (A&&P) s) := Φ s (i s x) (i s y). Global Instance equiv_rel_trace_congruence (s : Sort σ) : EquivRel ( s). Proof. unfold . constructor. - intros [y Y]. reflexivity. - intros [y1 Y1] [y2 Y2] S. by symmetry. - intros [y1 Y1] [y2 Y2] [y3 Y3] S T. by transitivity y2. Qed.
Require Import Import