search

felixwellen / synthetic-geometry

Synthetic geometry. Probably mostly algebraic geometry.
MIT License
23 stars 4 forks source link

Simplify simple-qc-open-prop #7

Closed MatthiasHu closed 2 years ago

MatthiasHu commented 2 years ago

Use create-qc-open-prop to define simple-qc-open-prop.

MatthiasHu commented 2 years ago

Oops, I forgot that we want fst (fst (simple-qc-open-prop x)) to simplify to x ∈ k ˣ!