proposition: Lemma term_of_string_fill : forall c s, term_of_string (SContext.fill c s) = fill (cont_of_string (lft c)) (sub (sub_of_string (rgt c)) (term_of_string s)).
proof: Proof. intros [l r] s. elim l; unfold SContext.fill; simpl. elim s. refl. intros. simpl. rewrite H. refl. intros. rewrite H, (Vcast_cons (cont_aux is_unary_sig a)), Vcast_refl. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN VecUtil ListUtil NatUtil)