I have this hypothesis: H : (x = s \/ x = t) /\ OoS v x. My current goal is OoS v s \/ OoS v t. So, my idea to solve it was to distribute the AND operator in H to get H : (x = s /\ OoS v x) \/ (x = t /\ OoS v x). And then I would transform this into: H : (OoS v s \/ OoS v t. And with auto, the proof would be done.
I searched for something useful with the command: Search _ ((?a \/ ?b) /\ ?c -> (?a /\ ?c) \/ (?b /\ ?c))., but I found nothing.
I solved the proof with something else, but I would like to know if such a thing is possible.
Did you try decompose [and or] H; subst; auto ?
You may also prove a distributivity lemma, then use rewrites.
Lemma and_or_dist (P Q R: Prop): (P \/ Q) /\ R <-> (P /\ R \/ Q /\ R).
Proof. tauto. Qed.
Require Import Setoid.
Goal forall x v s t, (x = s \/ x = t) /\ Oo5 v x -> Oo5 v s \/ Oo5 v t.
intros x v s t H; rewrite and_or_dist in H. (* ... *)