Commit 94768d56 authored by Ralf Jung's avatar Ralf Jung

fix transitivity change

parent 08b69a69
......@@ -52,7 +52,7 @@ Proof.
- intros [x y]. apply prod_lexico_irreflexive.
by apply (irreflexivity lexico y).
- intros [??] [??] [??] ??.
eapply prod_lexico_transitive; eauto. apply trans.
eapply prod_lexico_transitive; eauto. apply transitivity.
Qed.
Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)}
`{Lexico B, tB : !TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _).
......
......@@ -2493,7 +2493,7 @@ Section Forall2_order.
Global Instance: Symmetric R Symmetric (Forall2 R).
Proof. intros. induction 1; constructor; auto. Qed.
Global Instance: Transitive R Transitive (Forall2 R).
Proof. intros ????. apply Forall2_transitive. by apply @trans. Qed.
Proof. intros ????. apply Forall2_transitive. by apply @transitivity. Qed.
Global Instance: Equivalence R Equivalence (Forall2 R).
Proof. split; apply _. Qed.
Global Instance: PreOrder R PreOrder (Forall2 R).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment