Select All

Shift+Scroll to zoom
Shift+Click a node to highlight connections

Settings
dataset coq-tactician-stdlib.8.11.dev theories Init Logic
and_iff_compat_l
Proof
Download 
Type: (forall A B C : Prop, B <-> C -> A /\ B <-> A /\ C)
Term: (fun (A B C : Prop) (_tmp_tactician0 : B <-> C) => match _tmp_tactician0 with | conj Hl Hr => conj (fun _tmp_tactician1 : A /\ B => match _tmp_tactician1 with | conj H H0 => conj H (Hl H0) end) (fun _tmp_tactician1 : A /\ C => match _tmp_tactician1 with | conj H H0 => conj H (Hr H0) end) end)

Type: (forall A B C : Prop, B <-> C -> A /\ B <-> A /\ C)

Term: (fun (A B C : Prop) (_tmp_tactician0 : B <-> C) => match _tmp_tactician0 with | conj Hl Hr => conj (fun _tmp_tactician1 : A /\ B => match _tmp_tactician1 with | conj H H0 => conj H (Hl H0) end) (fun _tmp_tactician1 : A /\ C => match _tmp_tactician1 with | conj H H0 => conj H (Hr H0) end) end)

Rendering