diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/3854.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3854.v')
-rw-r--r-- | test-suite/bugs/closed/3854.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3854.v b/test-suite/bugs/closed/3854.v new file mode 100644 index 00000000..f8329cdd --- /dev/null +++ b/test-suite/bugs/closed/3854.v @@ -0,0 +1,21 @@ +Definition relation (A : Type) := A -> A -> Type. +Class Reflexive {A} (R : relation A) := reflexivity : forall x : A, R x x. +Axiom IsHProp : Type -> Type. +Existing Class IsHProp. +Inductive Empty : Set := . +Notation "~ x" := (x -> Empty) : type_scope. +Record hProp := BuildhProp { type :> Type ; trunc : IsHProp type }. +Arguments BuildhProp _ {_}. +Canonical Structure default_hProp := fun T P => (@BuildhProp T P). +Generalizable Variables A B f g e n. +Axiom trunc_forall : forall `{P : A -> Type}, IsHProp (forall a, P a). +Existing Instance trunc_forall. +Inductive V : Type := | set {A : Type} (f : A -> V) : V. +Axiom mem : V -> V -> hProp. +Axiom mem_induction +: forall (C : V -> hProp), (forall v, (forall x, mem x v -> C x) -> C v) -> forall v, C v. +Definition irreflexive_mem : forall x, (fun x y => ~ mem x y) x x. +Proof. + pose (fun x => BuildhProp (~ mem x x)). + refine (mem_induction (fun x => BuildhProp (~ mem x x)) _); simpl in *. + admit. |