blob: b08b7ab3cc4ff8453e5c70545a361e582e37facd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
Require Import FunctionalExtensionality.
Ltac make_apply_under_binders_in lem H :=
let tac := make_apply_under_binders_in in
match type of H with
| forall x : ?T, @?P x
=> let ret := constr:(fun x' : T =>
let Hx := H x' in
$(let ret' := tac lem Hx in
exact ret')$) in
match eval cbv zeta in ret with
| fun x => Some (@?P x) => let P' := (eval cbv zeta in P) in
constr:(Some P')
end
| _ => let ret := constr:($(match goal with
| _ => (let H' := fresh in
pose H as H';
apply lem in H';
exact (Some H'))
| _ => exact (@None nat)
end
)$) in
let ret' := (eval cbv beta zeta in ret) in
constr:(ret')
| _ => constr:(@None nat)
end.
Ltac apply_under_binders_in lem H :=
let H' := make_apply_under_binders_in lem H in
let H'0 := match H' with Some ?H'0 => constr:(H'0) end in
let H'' := fresh in
pose proof H'0 as H'';
clear H;
rename H'' into H.
Goal forall A B C (f g : forall (x : A) (y : B x), C x y), (forall x y, f x y = g x y) -> True.
Proof.
intros A B C f g H.
let lem := constr:(@functional_extensionality_dep) in
apply_under_binders_in lem H.
(* Anomaly: Uncaught exception Not_found(_). Please report. *)
|
