A ->B | forall x : D, A | A /\ B | False | |
Hypothesis | apply H | apply H | elim H case H destruct H as [H1 H2] |
elim H case H |
Goal | intro H intros |
intro x intros |
split |
~A | exists x:D, A | A\/B | |
Hypothesis | elim H case H |
elim H case H destruct H as [x H1] |
elim H case H destruct H as [H1 | H2] |
Goal | intro H intros |
exists t | left right |
t = q | |
Hypothesis | rewrite H rewrite <- H |
Goal | reflexivity ring |