blob: aa2b189b67c302e135050b08835c4f220d7433b2 (
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
|
(* Inductive t : Type -> Type := *)
(* | Just : forall (A : Type), t A -> t A. *)
(* Fixpoint test {A : Type} (x : t A) : t (A + unit) := *)
(* match x in t A return t (A + unit) with *)
(* | Just T x => @test T x *)
(* end. *)
Definition Type1 := Type.
Definition Type2 := Type.
Definition cast (x:Type2) := x:Type1.
Axiom f: Type2 -> Prop.
Definition A :=
let T := fun A:Type1 => _ in
fun A':Type2 =>
eq_refl : T A' = f A' :> Prop.
(* Type2 <= Type1... f A -> Type1 <= Type2 *)
Inductive t : Type -> Type :=
| Just : forall (A : Type), t A -> t A.
Fixpoint test {A : Type} (x : t A) : t (A + unit) :=
match x in t A with
| Just B x => @test B x
end.
|
