dep_well_formed_entrypoints_eq

Proof of dep_well_formed_entrypoints started from the scratch to make it clean and in sync with master