diff options
Diffstat (limited to 'theories/Wellfounded/Union.v')
| -rw-r--r-- | theories/Wellfounded/Union.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index d7f241dd0..6a6a9882f 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -26,7 +26,7 @@ Remark strip_commut : commut A R1 R2 -> forall x y:A, clos_trans A R1 y x -> - forall z:A, R2 z y -> exists2 y' : A | R2 y' x & clos_trans A R1 z y'. + forall z:A, R2 z y -> exists2 y' : A, R2 y' x & clos_trans A R1 z y'. Proof. induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros. elim H with y x z; auto with sets; intros x0 H2 H3. |