proposition: Theorem reduction : CD_TYP ⪯ CD_TC.
proof: Proof. exists (fun M => (nil, app (lam (lam (var 0))) (Nat.iter (var_bound M) lam M), arr (atom 0) nil (atom 0))). move=> M. split. - move=> [Gamma] [t] /var_bound_spec' /abs_Gamma_spec [t']. rewrite /= map_length seq_length=> ?. econstructor. + do 3 econstructor; first done. by left. + by eassumption. + by apply: Forall_nil. - move=> /= /type_assignmentE [] s phi _ + _. elim: (var_bound M) (nil) (s). { move=> ???. do 2 eexists. by eassumption. } move=> ? IH ? [?|???] /= /type_assignmentE; first done. by apply: IH. Qed.
imports: Undecidability.IntersectionTypes(CD Util.CD_facts) Undecidability.LambdaCalculus.Util.term_facts List PeanoNat Lia ssreflect Undecidability.Synthetic.Definitions