Commit 13c012d4 authored by Ralf Jung's avatar Ralf Jung

fix transitivity change

parent f7f79d26
......@@ -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.
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
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment