intros; cases x in H; [intros; reflexivity] intro; cases (?:False);
cases (q_le_cases ?? H);
[1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %);
intros; cases x in H; [intros; reflexivity] intro; cases (?:False);
cases (q_le_cases ?? H);
[1: apply (q_lt_corefl OQ); rewrite < H1 in ⊢ (?? %);