|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);
|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);