proposition: Lemma join_env_prop_right_rec : forall l l' g, compatible l l' -> forall r, i_a Ab.m g (to_a1 l r) -> i_a Ab.m g (to_a1 (l' @@ l) r).
proof: Proof. intros l l' g Hc; induction Hc; intros r; simpl; auto. destruct (str_in_list s r); simpl; auto. destruct (to_syn a1); intros [Ha1 Htl1]. destruct (to_syn (join a2 a1)); split; auto. i_a_to_to_p. apply Ab.thinner_prop with a1; auto. apply thinner_join_right; auto. to_p_to_i_a; exact Ha1. Qed.
imports: syntax little denot Bool List String ZArith axiom