proposition: Lemma aeq_gp_incl_aeq : aeq_gp << aeq.
proof: Proof. intros u v; revert u v; induction 1. refl. refl. rewrite IHaeq_gp1, IHaeq_gp2. refl. ens. revert IHaeq_gp. rewrite transpose_sym, transpose_sym with (x:=z). rewrite transpose_rename. 2-3: firstorder auto with set. rewrite transpose_rename. 2-3: firstorder auto with set. intro IH. rewrite aeq_alpha with (y:=z). 2: firstorder auto with set. rewrite IH, <- aeq_alpha; firstorder auto with crelations set. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)