proposition: Lemma successfull_hd_eq : forall x r1 r2, In r1 D -> In r2 D -> successfull (iter_step x (mk_problem (ren_cap r1 r2) (lhs r2))) = true -> hd_eq (rhs r1) (lhs r2) = true.
proof: Proof. intros x r1 r2 h1 h2 H. set (p := mk_problem (ren_cap r1 r2) (lhs r2)) in H. assert (problem_wf p). apply wf_mk_problem. destruct (successfull_is_sol H0 H). revert H1. unfold p, mk_problem, ren_cap. simpl. intuition. revert H1. rewrite forallb_forall in hypD. ded (hypD _ h1). ded (hypD _ h2). destruct r1 as [l1 r1]. destruct r2 as [l2 r2]. simpl. destruct r1. refl. destruct l2. refl. set (k := S (maxvar (Fun f0 t0))). rewrite ren_cap_fun. revert H1. unfold undefined_rhs, undefined. simpl. rewrite negb_lr. simpl. intro. rewrite H1. unfold is_sol_eqn. unfold fst, snd. rewrite !sub_fun. intro. Funeqtac. rewrite (beq_refl (@beq_symb_ok Sig)). refl. Qed.
imports: Coq(Lia Compare_dec) CoLoR(ADecomp AUnif ARenCap ATrs ListUtil RelUtil AGraph LogicUtil AShift ACalls BoolUtil ADuplicateSymb ListDec EqUtil AHDE)