Skip to content

Instantly share code, notes, and snippets.

@pirapira

pirapira/gist:1045359

Created June 24, 2011 18:23
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save pirapira/1045359 to your computer and use it in GitHub Desktop.
Save pirapira/1045359 to your computer and use it in GitHub Desktop.
Download ZIP
found the owner
Raw
gistfile1.txt
Parameter person :Set.
Parameter thing: Set.
Parameter bottle: thing.
Parameter own: person -> thing -> Prop.
Parameter capitalist: forall (x: thing), { p:person & own p x }.
Definition owner: person.
generalize (capitalist bottle).
intros.
destruct H.
assumption.
Defined.
Lemma owner_owns_bottle: own owner bottle.
unfold owner.
generalize (capitalist bottle).
intros.
destruct s.
assumption.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment