proposition: Lemma wf_add_pair: forall R, well_founded R -> forall i j, ~ clos_refl_trans T R j i -> well_founded (add_pair i j R).
proof: Proof. intros R Hwf i j Hij. assert (Hi: forall v, clos_refl_trans _ R v i -> Acc (add_pair i j R) v). induction v as [v IH] using (well_founded_induction Hwf); intros Hui. constructor. intros u [[-> ->]|Huv]. elim Hij. assumption. apply IH. assumption. eauto using rt_trans, rt_step. intro v. induction v as [v IH] using (well_founded_induction Hwf). constructor. intros u [[-> ->] | Huv]. apply Hi. constructor 2. apply IH. assumption. Qed.
imports: ATBR(Common)