blob: ad4778cc36a6a76afda37f950c123fdf7e72120d (
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
|
Set Implicit Arguments.
Generalizable Variables A.
Parameter val : Type.
Class Enc (A:Type) :=
make_Enc { enc : A -> val }.
Global Instance Enc_dummy : Enc unit.
Admitted.
Definition FORM := forall A (EA:Enc A) (Q:A->Prop), Prop.
Axiom FORM_intro : forall F : FORM, F unit Enc_dummy (fun _ : unit => True).
Definition IDF (F:FORM) : FORM := F.
Parameter ID : forall (G:Prop), G -> G.
Parameter EID : forall A (EA:Enc A) (F:FORM) (Q:A->Prop),
F _ _ Q ->
F _ _ Q.
Lemma bla : forall F,
(forall A (EA:Enc A), IDF F EA (fun (X:A) => True) -> True) ->
True.
Proof.
intros F M.
notypeclasses refine (M _ _ _).
notypeclasses refine (EID _ _ _ _).
eapply (ID _).
Unshelve.
+ apply FORM_intro.
Qed.
|
