proposition: Lemma refine_UpdateUnConstrRelationDeleteC {qsSchema} : forall (qs : UnConstrQueryStructure qsSchema) (Ridx : Fin.t (numRawQSschemaSchemas qsSchema)) (deletedTuples : Ensemble RawTuple), refine (UpdateUnConstrRelationDeleteC qs Ridx deletedTuples) (ret (UpdateUnConstrRelation qs Ridx (EnsembleDelete (GetUnConstrRelation qs Ridx) deletedTuples))).
proof: Proof. reflexivity. Qed.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory