{P : Sort u} →
  {Context : Sort u_1} →
    {ctx : Context} →
      {t : LLVM.Builder ctx} →
        {Context' : Sort u_1} →
          {ctx' : Context'} →
            {t' : LLVM.Builder ctx'} → Context = Context' → ctx ≍ ctx' → t ≍ t' → LLVM.Builder.noConfusionType P t t'