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 term_of_string. rewrite H, sub_fun1. refl. unfold SContext.fill. simpl lft. simpl rgt. intros. simpl term_of_string. simpl cont_of_string. rewrite fill_cont1. apply args_eq. apply Vcast_eq_intro. apply Vcons_eq_intro. 2: refl. hyp. Qed.
imports: CoLoR(LogicUtil RelUtil SN ListUtil Srs ATrs AUnary VecUtil EqUtil NatUtil ListMax)