proposition: Lemma term_gt_incl_succ : term_gt << IR_succ.
proof: Proof. intros l r lr v. destruct (mint_eval_equiv l r v). simpl in *. unfold succ. unfold succ_vec. symmetry in H. symmetry in H0. rewrite (Vforall2_aux_Proper gtx_mor _ _ H _ _ H0). apply mint_eval_mon_succ. hyp. Qed.
imports: CoLoR(AMonAlg Matrix OrdSemiRing VecUtil SN RelUtil LogicUtil AMatrixBasedInt) Coq(Setoid Morphisms)