-
François Bobot authored
(exists x. x=t and F) -> F[t/x] (forall x. x<>t or F) -> F[t/x] Cette transformation n'élimine pas les quantifications qui ont des triggers mais s'applique sous ces derniers. Le but est de pouvoir éliminer les quantifications inutilement ajoutées lors de eliminate inductive.
95c2ea8f