proposition: Lemma UpdateUnConstrRelation_Abstract_AbsR {qsSchema} : forall (r_o : UnConstrQueryStructure qsSchema) (r_n : Iterate_Dep_Type_BoundedIndex _), UnConstryQueryStructure_Abstract_AbsR r_o r_n -> forall idx R, UnConstryQueryStructure_Abstract_AbsR (UpdateUnConstrRelation r_o idx R) (Update_Iterate_Dep_Type idx _ r_n R).
proof: Proof. intros. destruct qsSchema; simpl in *. unfold UnConstryQueryStructure_Abstract_AbsR in *. unfold UnConstrQueryStructure in r_o; simpl in *. unfold UpdateUnConstrRelation; simpl. simpl; clear qschemaConstraints. generalize dependent qschemaSchemas; intro. revert idx; induction qschemaSchemas; simpl; intros. - inversion idx. - generalize dependent idx. intro; intro. generalize dependent qschemaSchemas. pattern n, idx. lazymatch goal with | [ |- ?P _ idx ] => simpl; eapply (@Fin.caseS P); simpl; intros; intuition end. Qed.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory