proposition: Lemma duplicate_type_in t v ls : List.In (existT _ (t, t) v) (duplicate_type ls) -> List.In (existT _ t v) ls.
proof: Proof. unfold duplicate_type; rewrite List.in_map_iff. intros [ [? ?] [? ?] ]. inversion_sigma; inversion_prod; inversion_TypeCode; subst; simpl. assumption. Qed.
imports: Coq.Lists.List Coq.Arith.EqNat Coq.Logic.Eqdep_dec Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.SyntaxEquality Fiat.Parsers.Reflective.SyntaxEquivalence Fiat.Common.PointedProp Fiat.Common.OptionFacts Fiat.Common.Prod Fiat.Common.Sigma Fiat.Common