test-suite/success/DHyp.v


1
2
3
4
5
6
7
8
9
10
11
12

HintDestruct Hypothesis h1 (le ? O) 3 [Fun I -> Inversion I ].

Lemma lem1 : ~(le (S O) O).
Intro H.
DHyp H.
Qed.

HintDestruct Conclusion h2 (le O ?) 3 [Constructor].

Lemma lem2 : (le O O).
DConcl.
Qed.