diff options
Diffstat (limited to 'test-suite/bugs/closed/4596.v')
-rw-r--r-- | test-suite/bugs/closed/4596.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4596.v b/test-suite/bugs/closed/4596.v new file mode 100644 index 00000000..592fdb65 --- /dev/null +++ b/test-suite/bugs/closed/4596.v @@ -0,0 +1,14 @@ +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. + +Definition T (x : bool) := x = true. + +Goal forall (S : Type) (b b0 : S -> nat -> bool) (str : S) (p : nat) + (s : forall n : nat, bool) + (s0 s1 : nat -> S -> S), + (forall (str0 : S) (n m : nat), + (if s m then T (b0 (s1 n str0) 0) else T (b (s1 n str0) 0)) -> T (b (s0 n str0) m) -> + T (b str0 m)) -> + T (b str p). +Proof. +intros ???????? H0. +rewrite H0. |