proposition: Fact dc_eval_ext c φ1 ν1 φ2 ν2 : (forall x, dc_vars c x -> φ1 x = φ2 x) -> (forall x, ν1 x = ν2 x) -> dc_eval φ1 ν1 c <-> dc_eval φ2 ν2 c.
proof: Proof. intros H1 H2. destruct c as (v,e); unfold dc_eval; simpl. rewrite H1; simpl; auto. rewrite dee_eval_ext with e φ1 ν1 φ2 ν2; try tauto. intros; apply H1; simpl; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)