db38bc4043
We should not allow `h.1` if `h` is a proposition and the result is not. The recursor for `h`'s type can only eliminate into `Prop`.
3 lines
155 B
Text
3 lines
155 B
Text
def foo (h : ∃ x: Nat, True) := h.1
|
|
theorem contradiction : False :=
|
|
(by decide : 0 ≠ 1) (show foo ⟨0, trivial⟩ = foo ⟨1, trivial⟩ from rfl)
|