0
Disons que ce sont mes locaux et objectifs actuels:Réécriture hypothèse avec une expression plus concrète
IHl' : forall l' : list A, In a l'' \/ In a l' -> In a (l'' ++ l')
l' : list A
============================
....
Maintenant, je veux l'hypothèse de se transformer comme ceci:
IHl' : In a l'' \/ In a l' -> In a (l'' ++ l')
l' : list A
============================
....
Donc, au fond, je instancier IHl' avec l'. Y a-t-il une tactique qui fait cela? Réécrire ou même introduire une nouvelle hypothèse spécialisée devrait faire l'affaire.
Ce type de question surgit de temps en temps ici. Voici une liste (éventuellement incomplète) de questions dans l'ordre chronologique, qui pourrait vous aider: [1] (http://stackoverflow.com/questions/15573794/), [2] (http://stackoverflow.com/questions/19053778 /), [3] (http://stackoverflow.com/questions/20156622/), [4] (http://stackoverflow.com/questions/25687981/), [5] (http: // stackoverflow .com/questions/29316168 /), [6] (http://stackoverflow.com/questions/35994491/), [7] (http://stackoverflow.com/questions/39904991/), [8] (http : //stackoverflow.com/questions/40448703/). –
@AntonTrunov BTW Certaines de ces questions ne devraient-elles pas être marquées comme des doublons d'autres questions? –
@ Zimmi48 Je pense que vous avez raison. Je voulais juste augmenter la connectivité (cela peut entraîner de meilleurs résultats de recherche). N'hésitez pas à signaler les questions si vous le jugez approprié :) –