A note on subject reduction in (→,∃)-Curry with respect to complete developments

We prove subject reduction of the Curry style existential system (→,∃) with regard to complete developments. We use here a remote adaptation of the technique of Barbanera et al. used before for systems with union types.