Coq: How to apply axioms deeper in the goal?

Question

Trying to prove MT1A with MT1 (or MT1bis), but Coq fails to unify:

Require Export Classical_Prop.
Require Export Classical_Pred_Type.

Variable MT : Type.
Parameter NIL : MT.
Variables a b e : MT -> MT.
Variable c : MT * MT -> MT.

Axiom MT1 :
  forall x y z: MT, z = c(x,y) -> a(z) = x /\ b(z) = y.

Axiom MT1bis :
  forall x y z: MT, z = c(x,y) <-> a(z) = x /\ b(z) = y.

Axiom MT3 :
  forall x y z : MT, z = c(a(z),b(z)) <-> a(z) <> z /\ b(z) <> z.

Definition example := c(NIL, e NIL).

Lemma MT1A :
  forall x: MT, x = a (c(example, b example)) -> x = example /\ a x <> x /\ b x <> x.
Proof.
(*  unfold example. *)
  intros.
  apply MT1. (* ??? *)

Qed.

Which tactics can be used here to hint Coq how to get c() out of a()? (One possibility also is, that those axioms are not enough for the proof, though at first glance they are. If MT1 is not enough, maybe MT1bis is?)

Tried to find suitable tactics, like rewrite, but it did not work (maybe, needed more complex hint). Can't find any more tactics, which can help.

(this is not homework assignment, just one hobby project)

Answer 1

I removed unused variables from MT3:

Axiom MT3 :
  forall z : MT, z = c(a(z),b(z)) <-> a(z) <> z /\ b(z) <> z.

We can use the remember tactic to kind of "extract" a term from inside a larger term (and remember this connection in an equation):

Lemma MT1A x :
  x = a (c (example, b example)) ->
  x = example /\ a x <> x /\ b x <> x.
Proof.
  unfold example; intros H.
  rewrite <-MT3.
  remember (c (NIL, e NIL)) as f eqn:F.
  pose proof (MT1 _ _ _ F) as [F1 F2].
  remember (c (f, b f)) as g eqn:G.
  pose proof (MT1 _ _ _ G) as [G1 G2].
  split; congruence.
Qed.