yellowsquid/cfe-proof.git/src/Cfe/Context, branch lemma3.5 [no description] http://git.yellowsquid.uk/yellowsquid/cfe-proof.git/atom?h=lemma3.5 2021-03-23T14:14:17Z Prove substitution into guarded variable. 2021-03-23T14:14:17Z Chloe Brown chloe.brown.00@outlook.com 2021-03-23T14:14:17Z urn:sha1:da0c9709fc93676587c1505de688d7d1f7a33489 Replace transfer with shift. 2021-03-23T12:19:30Z Chloe Brown chloe.brown.00@outlook.com 2021-03-23T12:19:30Z urn:sha1:a92f724a46a78af74121c44bbb06c4ec51f9555e Prove substitution in the unguarded context. Prove transfer. 2021-03-22T16:43:49Z Chloe Brown chloe.brown.00@outlook.com 2021-03-22T16:43:49Z urn:sha1:9e89f36e3fc6210b270d673c30691530015278fb Prove judgement weakening. 2021-03-21T13:14:22Z Chloe Brown chloe.brown.00@outlook.com 2021-03-21T13:14:22Z urn:sha1:9c72c8ed0c3e10b5dafb41e438285b08f244ba68 Separate Context into a different module. 2021-03-20T18:36:24Z Chloe Brown chloe.brown.00@outlook.com 2021-03-20T18:36:24Z urn:sha1:4e0ceac75e6d9940f0e11f93a3815448df258c70