Skip to content
Snippets Groups Projects
Commit 6567ed5b authored by Quentin VERMANDE's avatar Quentin VERMANDE
Browse files

duplicate clear

parent e7841de1
Branches
Tags
No related merge requests found
Pipeline #119363 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/logrel/F_mu_ref_conc/binary/fundamental.v
+ 1
− 1
View file @ 6567ed5b
...@@ -560,7 +560,7 @@ Section fundamental. ...@@ -560,7 +560,7 @@ Section fundamental.
Theorem binary_fundamental Γ e τ : Theorem binary_fundamental Γ e τ :
Γ ⊢ₜ e : τ → ⊢ Γ ⊨ e ≤log≤ e : τ. Γ ⊢ₜ e : τ → ⊢ Γ ⊨ e ≤log≤ e : τ.
Proof. Proof.
elim=> {Γ e τ} Γ. elim=> {}Γ {e τ}.
- intros; iApply bin_log_related_var; done. - intros; iApply bin_log_related_var; done.
- iApply bin_log_related_unit. - iApply bin_log_related_unit.
- intros; iApply bin_log_related_int. - intros; iApply bin_log_related_int.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment