A : Prop
B : Prop
C : Prop
_tmp_tactician0 : (B <-> C)
----------------------
(A /\ B <-> A /\ C)
Raw: A : Prop, B : Prop, C : Prop, _tmp_tactician0 : (B <-> C) |- (A /\ B <-> A /\ C)
A : Prop
B : Prop
C : Prop
Hl : (B -> C)
Hr : (C -> B)
----------------------
(A /\ B <-> A /\ C)
Raw: A : Prop, B : Prop, C : Prop, Hl : (B -> C), Hr : (C -> B) |- (A /\ B <-> A /\ C)
match _tmp_tactician0 with | conj Hl Hr => _ end