Lemma ex1_a : forall A B C: Prop, A/\(B/\C)->(A/\B)/\C.
Proof.
  intros a b c H.
  destruct H as [A H2].
  destruct H2 as [B C].
  split.
     split.
     exact A.
  exact B.
  exact C.
Qed.

Lemma ex1_b : forall A B C: Prop, A /\ (B /\ C) -> (A /\ B) /\ C.
intuition.
Qed.

Lemma ex2: forall A B C D: Prop, (A->B)/\(C->D)/\A/\C -> B/\D.
Proof.
intros a b c d H.
destruct H as [I1 H2].
destruct H2 as [I2 ac].
destruct ac as [A C].
split.
apply I1.
assumption.
apply I2; assumption.

Check (3::nil).
Check cons.
Locate "_ :: _".
Open Scope list_scope.

Locate "_ * _".
Check (1::2::3::nil).
----   (* stopped here *)