lean2/tests/lean/j5.lean

theorem or_imp2 (p q : Bool) : (p ∨ q) ↔ (¬ p → q)
:= subst (symm (imp_or (¬ p) q)) (not_not_eq p)
refactor(builtin/kernel): use standard definition for 'or' and 'and' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-02-17 20:05:34 +00:00				`theorem or_imp2 (p q : Bool) : (p ∨ q) ↔ (¬ p → q)`
fix(library/elaborator): bug reported by Jeremy Avigad Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-02-10 22:01:08 +00:00				`:= subst (symm (imp_or (¬ p) q)) (not_not_eq p)`