blob: 5c23f8404b884fed9904f5a917f14881e83ee9c7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* -*- coq-prog-args: ("-emacs" "-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *)
Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality.
Set Printing Universes.
Inductive Foo (I : Type -> Type) (A : Type) : Type :=
| foo (B : Type) : A -> I B -> Foo I A.
Definition Family := Type -> Type.
Definition FooToo : Family -> Family := Foo.
Definition optionize (I : Type -> Type) (A : Type) := option (I A).
Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A.
Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
Definition barRec : Rec (optionize id) := {| rec := bar id |}.
Inductive Empty {T} : T -> Prop := .
Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family)
nil)) (b : unit) :
Empty (a, b) -> False.
Proof.
intro e.
dependent induction e.
Qed.
|
