Commit 25bdb78f authored by Ralf Jung's avatar Ralf Jung

remove some redundant parentheses

parent 6be2994e
Pipeline #10278 passed with stage
in 16 minutes and 46 seconds
...@@ -160,7 +160,7 @@ Notation "'∃..' x .. y , P" := (texist (λ x, .. (texist (λ y, P)) .. )) ...@@ -160,7 +160,7 @@ Notation "'∃..' x .. y , P" := (texist (λ x, .. (texist (λ y, P)) .. ))
format "∃.. x .. y , P") : stdpp_scope. format "∃.. x .. y , P") : stdpp_scope.
Lemma tforall_forall {TT : tele} (Ψ : TT Prop) : Lemma tforall_forall {TT : tele} (Ψ : TT Prop) :
(tforall Ψ) ( x, Ψ x). tforall Ψ ( x, Ψ x).
Proof. Proof.
symmetry. unfold tforall. induction TT as [|X ft IH]. symmetry. unfold tforall. induction TT as [|X ft IH].
- simpl. split. - simpl. split.
...@@ -173,7 +173,7 @@ Proof. ...@@ -173,7 +173,7 @@ Proof.
Qed. Qed.
Lemma texist_exist {TT : tele} (Ψ : TT Prop) : Lemma texist_exist {TT : tele} (Ψ : TT Prop) :
(texist Ψ) (ex Ψ). texist Ψ ex Ψ.
Proof. Proof.
symmetry. induction TT as [|X ft IH]. symmetry. induction TT as [|X ft IH].
- simpl. split. - simpl. split.
......
Markdown is supported
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