module DuplicateInductiveParameterName; inductive T (A : Type) (B : Type) (A : Type) {}; end;