lean4-htt/tests/lean/run/specialize2.lean at deb77b62df75d03a101d028fd0b29ea3fed3678d - max/lean4-htt - maxgit: wireguard access, git repository.

max/lean4-htt

Leonardo de Moura bbe6d37109 fix: specialize

2021-09-11 19:52:51 -07:00

11 lines

320 B

Text

Raw Blame History

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

 example : (p → q → False) ↔ (¬ p ∨ ¬ q) := by
   apply Iff.intro
   . intro h
     byCases hp:p <;> byCases hq:q
     . specialize h hp hq; contradiction
     . exact Or.inr hq
     . exact Or.inl hp
     . exact Or.inr hq
   . intro
     | Or.inl hnp => intros; contradiction
     | Or.inr hnq => intros; contradiction