Module DupCapZeroWeight

Set Implicit Arguments.
Require Import MyTactics.
Require Import Layers.
Require Import RawPrograms.
Require Import Resources.
Require Import ResourcesContinued.
Require Import Environments.
Require Import Multiplicity.
Require Import Typing.
Require Import WellLayeredness.
Require Import InversionClassification.
Require Import Erasure.
Require Import ValueReductionTerminates.


Lemma zero_plus_zero:
  forall n1 n2,
  n1 = 0 ->
  n2 = 0 ->
  n1 + n2 = 0.

Local Hint Resolve zero_plus_zero duplicable_own_region
duplicable_own_location duplicable_split_left duplicable_split_right
duplicable_neutral.

Lemma duplicable_capabilities_have_zero_weight:
  forall R v T,
  jv R nil nil v T ->
  duplicable R ->
  wlv nil v Logical ->
  weight v = 0.