(**************************************************************************)
set "baseuri" "cic:/matita/tests/decompose".
(**************************************************************************)
set "baseuri" "cic:/matita/tests/decompose".
theorem stupid:
\forall a,b,c:Prop.
(a \land c \lor b \land c) \to (c \land (b \lor a)).
intros.decompose.split.assumption.right.assumption.
split.assumption.left.assumption.qed.
theorem stupid:
\forall a,b,c:Prop.
(a \land c \lor b \land c) \to (c \land (b \lor a)).
intros.decompose.split.assumption.right.assumption.
split.assumption.left.assumption.qed.