gdp
gdp copied to clipboard
Proof has phantom role
bad :: Proof p -> Proof q
bad = coerce
contra :: Proof FALSE
contra = coerce true