proposition: Lemma IR_context_closed : monotone -> context_closed IR.
proof: Proof. unfold transp, context_closed, IR. intros. gen (H0 xint). clear H0. intro. induction c. simpl. exact H0. simpl fill. simpl. do 2 (rewrite Vmap_cast, Vmap_app). simpl. apply H. exact IHc. Qed.
imports: CoLoR(ATerm RelUtil ASubstitution NaryFunction AContext VecUtil SN ARelation LogicUtil) Coq(Lia PeanoNat)