CODEWITHSUNDEEP
coq
Julian Stecklina
Julian Stecklina

Reputation: 1281

Applying an implication from a hypothesis

My coq proof currently looks like this:

a0 : nat
a1 : nat
n : nat
l : list nat
c : nat -> nat -> bool
H : forall a0 a1 a2 : nat,
    Is_true (c a0 a1) /\ Is_true (c a1 a2) -> Is_true (c a0 a2)
H0 : Is_true (c a1 a0)
H1 : Is_true (c a0 n)
============================
 Is_true (c a1 n)

How can I 'apply' H and finish the proof?

Upvotes: 0

Views: 836

Answers (1)

Ptival
Ptival

Reputation: 9447

You could do:

apply (H _ _ _ (conj H0 H1)).

Or:

exact (H _ _ _ (conj H0 H1)).

But that would be similar to doing:

apply H; assumption.

Or anything similar. I am not sure what the point of your question is exactly. Did I miss a detail?

Upvotes: 1

Related Questions