Branch where sm_inject_separated is deleted from the clause effcore_diagram, and is weakened to globals_separate in clause afterExternal
Pushing changes through Inlining
Pushed gloabls_separated through the file.
Updated atExternal.
ALL new admits proven.
Only [initial_core] left to be proven.
Inlining completely proved.
Adapted Tunneling
Heavy cleaning file Inlining...
More cleaning:
Organized lemmas.
Removed unused lemmas.
Removed all printing statements.
Removed unnecessary comments.
Some minor refactoring.
Added InliningproofEFF.v to Makefile
Adapted RTLgen
Adapted Renumber
Adapted Tailcall
Adapted Linearize
Adapted CleanupLabels
Adapted Stacking: several lemmas depended on sm_inject_separated
moved/renamed some lemmas, corected Tailcall, added CSE
Adapted [effect_corediagram_trans]
Incomplete changes for the other files.
Couldn't complete the AfterExternal in the transitivity proof.
Merge branch 'GlobalsSeparate' into NoRestrict

Conflicts:
	Makefile
	backend/InliningproofEFF.v
	core/effect_corediagram_trans.v
	core/effect_interpolants.v
	core/effect_simulations.v
	core/effect_simulations_lemmas.v
	core/effect_simulations_trans.v