lean2/tests/lean/simplifier6.lean.expected.out

5 lines
75 B
Text
Raw Permalink Normal View History

H1
imp_congr H1 H2
imp_congr H1 (imp_congr H2 H3)
forall_congr (λ x, H x)