blob: 592fdb6580d5a4b0ebbfda852fd8d6eb384cbdd0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
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.
|
