(* 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?
Hola.
Para poder usar la información de H deberías hacer análisis de casos en la/s variable/s booleanas que aparecen en el And; de lo contrario no vas a poder usar la información del And, que se define sobre valores true / false.
Quizás te convenga iniciar la prueba usando "case". Al tener el And instanciado podés usar simpl.
Saludos, Carlos
