proposition: Lemma aeq_incl_aeq_gp : aeq << aeq_gp.
proof: Proof. intro u; revert u. ind_size1 u; intros u' uu'; inv_aeq uu'; subst. refl. refl. apply aeq_gp_app; firstorder auto with crelations. set (xs := union (union (add x (union (fv u) (bv u))) (add x0 (union (fv u0) (bv u0)))) (union (fv (rename x x0 u)) (bv (rename x x0 u)))). gen (var_notin_ok xs). set (z := var_notin xs). unfold xs. set_iff. split_all. apply aeq_gp_lam with (z:=z). ens. set_iff. split_all. apply hu. unfold Def.transpose. rewrite size_action. refl. rewrite i0, transpose_sym. rewrite transpose_rename; auto. rewrite transpose_sym. rewrite transpose_rename; auto. rewrite rename2. refl. auto. apply aeq_gp_lam with (z:=z). ens. set_iff. split_all. apply hu. unfold Def.transpose. rewrite size_action. refl. rewrite i0, transpose_sym. rewrite transpose_rename; auto. rewrite transpose_sym. rewrite transpose_rename; auto. rewrite rename2. refl. auto. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)