| intros; simplify; split; intros; simplify;
[ change with (∀x. x ♮a b → x ♮a' b'); intros;
apply (. (#‡e1^-1)); whd in e; apply (if ?? (e ??)); assumption
| change with (∀x. x ♮a' b' → x ♮a b); intros;
apply (. (#‡e1)); whd in e; apply (fi ?? (e ??));assumption]]
qed.
| intros; simplify; split; intros; simplify;
[ change with (∀x. x ♮a b → x ♮a' b'); intros;
apply (. (#‡e1^-1)); whd in e; apply (if ?? (e ??)); assumption
| change with (∀x. x ♮a' b' → x ♮a b); intros;
apply (. (#‡e1)); whd in e; apply (fi ?? (e ??));assumption]]
qed.