corrade-nucleus-nucleons – Blame information for rev 20
?pathlinks?
| Rev | Author | Line No. | Line |
|---|---|---|---|
| 20 | office | 1 | import logic |
| 2 | section |
||
| 3 | variables (A : Type) (p q : A → Prop) |
||
| 4 | |||
| 5 | example : (∀x : A, p x ∧ q x) → ∀y : A, p y := |
||
| 6 | assume H : ∀x : A, p x ∧ q x, |
||
| 7 | take y : A, |
||
| 8 | show p y, from and.elim_left (H y) |
||
| 9 | end |