Proof Reuse with Extended Inductive Types

Proof assistants based on type theory such as Coq or Lego, putemphasis on inductive specifications and proofs by featuringexpressive inductive types. It isfrequent to modify an existing specification or proof by adding ormodifying constructors in inductive types. In the context of language design,adding constructors is a common practice to make progress step-by-step.In this article, we propose amechanism to extend and parameter inductive types, and aproof reuse mechanism founded on proof terms reuse