[Agda] Introducing hypotheses

[Philippe de Rochambeau]

Hello,

I am attempting to translate a Coq proof into Agda, for learning purposes (cf. https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf, p. 9):

tauto₁ : ∀ (A B C : Set) → (A → B → C) → (A → B) → A → C
tauto₁ = { }0

Here’s how Coq introduces hypotheses, letting the use apply them.

Coq < apply H’.
1 subgoal
A : Prop
B : Prop
C : Prop
H : A -> B -> C
H’ : A -> B
HA : A
============================
A

How do you do the same thing in Agda?

Cheers,

Philippe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200418/782dc62b/attachment.html>