search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
90 stars 18 forks source link

Automatically generated hypotheses conflict with user-named ones #145

Closed lambdacalculator closed 1 year ago

lambdacalculator commented 1 year ago

After

Theorem test : forall (A B:o) L, member A L -> member B L -> member A L.
intros H1.

the proof state is

Variables: A B L
H1 : member A L
H1 : member B L
============================
 member A L

At this point both clear H1 and case H1 remove both hypotheses (but the latter does inversion on the first).