few more steps

[helm.git] / helm / software / matita / contribs / dama / dama / ordered_set.ma

diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma
index a820eff542c5a94c93843f58364883546d86ae10..a227af3c1928927fe04185224cfe1b409d9b8029 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/ordered_set.ma
+++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma
@@ -52,7 +52,7 @@ qed.
 lemma square_ordered_set: ordered_set → ordered_set.
 intro O;
 apply (mk_ordered_set (O × O));
-[1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y);
+[1: intros (x y); apply (\fst x ≰ \fst y ∨ \snd x ≰ \snd y);
 |2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
     cases H (X X); apply (os_coreflexive ?? X);
 |3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2);