(* 2. LAnd : forall a b : bool, And a b = true <-> a = true /\ b = true *)
Lemma LAnd : forall a b : bool, And a b = true <-> a = true /\ b = true.
Proof.
intros.
unfold iff.
split.
intros.
split.
Llego hasta aquí y me tranco...como abro el And de la hipotesis H?