blob: b4414a6a1d83b79164c547d42163fa612eb51b8d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
intros A B H ?%H H0.
exact H1.
Qed.
Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
intros A B H ?H%H H0.
exact H1.
Qed.
Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
intros A B H J%H H0.
exact J.
Qed.
Set Mangle Names.
Goal forall (A B : Prop) (H : A -> B), A -> A -> B.
intros A B H ?%H _0.
assumption.
Qed.
|
