|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);
|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X);
|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;
|2: intro x; simplify; intro; cases H (X X); clear H; apply (bs_coreflexive ?? X);
|3: intros 2 (x y); simplify; intro H; cases H (X X); clear H; [left|right] apply (bs_symmetric ??? X);
|4: intros 3 (x y z); simplify; intro H; cases H (X X); clear H;