proposition: Lemma andX (a b : bool) : reflect (a * b) (a && b).
proof: Proof. by case: a; case: b; constructor=>//; case. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)