proposition: Lemma t1_le_t2 : itree_le t1 t2.
proof: Proof. unfold t1, t2; constructor; auto with zarith. intro i; exists (2 * i); unfold isingle; constructor. - auto with zarith. - exists i;constructor. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith