proposition: Lemma t1_le'_t2 : itree_le' t1 t2.
proof: Proof. unfold t1, t2; constructor 2 with (fun i : nat => 2 * i); auto with zarith. unfold isingle; intro i ; constructor 2 with (fun i :nat => i); auto with zarith. constructor . Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith