proposition: Lemma are_constructors_of_R : forall R, (forall v t, ~ R t (Var v)) -> forall f l t', (refl_trans_clos (one_step R) t' (Term f l)) -> (~defined R f) -> exists l', t' = Term f l' /\ refl_trans_clos (one_step_list (one_step R)) l' l.
proof: Proof. intros R R_var f l t' H Cf. inversion H as [u | u1 u2 K]; clear H; subst. exists l; split; [reflexivity | left]. set (t := Term f l) in *. assert (H := eq_refl t). unfold t at 2 in H. clearbody t; revert H; induction K as [u1 u2 K1 | u1 u2 u3 K1 Kn]; intros; subst. inversion K1 as [v1 v2 K | g k1 k2 K]; clear K1; subst. inversion K as [v1 v2 sigma H]; clear K. destruct v2 as [x2 | f2 l2]. apply False_rect; apply (R_var _ _ H). apply False_rect; apply Cf; injection H1; clear H1; intros; subst; constructor 1 with l2 v1; assumption. exists k1; split; [reflexivity | right; left; assumption]. destruct (IHKn (eq_refl _)) as [l' [H1 H2]]; clear IHKn; subst. inversion K1 as [v1 v2 K | g k1 k2 K]; clear K1; subst. inversion K as [v1 v2 sigma H]; clear K. destruct v2 as [x2 | f2 l2]. apply False_rect; apply (R_var _ _ H). apply False_rect; apply Cf; injection H1; clear H1; intros; subst; constructor 1 with l2 v1; assumption. exists k1; split; [reflexivity | apply refl_trans_clos_is_trans with l']. right; left; assumption. assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)