Better induction /// exists for existT

uwplse / PUMPKIN-PATCH

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

MIT License

51 stars 2 forks source link

Closed randair closed 4 years ago

randair commented 4 years ago

induction works for motives expecting more than was passed as final arguments (aka rev_app_distr actually works)
Px ==> Px' |- existT A P x Px ==> exists x. Px' (best attempt at semantics heh)
reflexivity moved to first pass
fixed environment related bugs