Commit ce6f4e19 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso Committed by Ralf Jung
Browse files

fix spacing

parent 89b76adb
......@@ -731,7 +731,7 @@ Section sep_list2.
intros HΦ. apply (anti_symm _).
{ apply and_intro; [apply big_sepL2_length|].
apply forall_intro=> k. apply forall_intro=> x1. apply forall_intro=> x2.
do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply :big_sepL2_lookup. }
do 2 (apply impl_intro_l; apply pure_elim_l=> ?). by apply: big_sepL2_lookup. }
apply pure_elim_l=> Hlen.
revert l2 Φ HΦ Hlen. induction l1 as [|x1 l1 IH]=> -[|x2 l2] Φ HΦ Hlen; simplify_eq/=.
{ by apply (affine _). }
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment