(motive : Qq.Impl.MVarSynth → Sort u_1) →
  (synth : Qq.Impl.MVarSynth) →
    ((quotedType : Lean.Expr) → (exprMVar : Lean.MVarId) → motive (Qq.Impl.MVarSynth.term quotedType exprMVar)) →
      ((exprMVar : Lean.MVarId) → motive (Qq.Impl.MVarSynth.type exprMVar)) →
        ((x : Qq.Impl.MVarSynth) → motive x) → motive synth