proposition: Lemma join_env_prop_right : forall l l' g, compatible l l' -> i_a Ab.m g (to_a l) -> i_a Ab.m g (to_a (l' @@ l)).
proof: Proof. intros l l' g Hc; exact (join_env_prop_right_rec l l' g Hc nil). Qed.
imports: syntax little denot Bool List String ZArith axiom