small changes

src/LeanSupportEquivalence.v

@@ -43,8 +43,8 @@ Lemma wf_make_seq_infSub {l} (inner: infSub l) :
 
 
 (*** GET LIST OF PORTS ***)
-Definition make_seq_Port_for_node_n {s i r o} {b:bigraph s i r o} (n:get_node b) : 
-  seq (Port (get_control (bg:=b))) := map 
+Definition make_seq_Port_for_node_n {s i r o} {b:bigraph s i r o} (n:get_node b) : seq (Port (get_control (bg:=b))) := 
+  map 
     (fun port => existT (fun n => 'I_(Arity (get_control (bg:=b) n))) n (port)) 
     (ord_enum (Arity (get_control (bg:=b) n))).
 
@@ -183,7 +183,7 @@ Lemma not_is_idle_implies_exists_inner_or_node {s i r o} {b:bigraph s i r o} (e:
   by apply/eqP.
   Qed.
   
-Definition get_edges_wo_idles {s i r o} (b:bigraph s i r o) := 
+Definition get_edges_wo_idles {s i r o} (b:bigraph s i r o) : finType := 
   {e : get_edge b | not_is_idle e}.
 
 
@@ -201,7 +201,8 @@ Definition lean {s i r o} (b:bigraph s i r o) :
     _
     (get_ap (bg:=b))).
   intros ip'.
-  assert (exists ip'', get_link (bg:=b) ip'' = get_link (bg:=b) ip') as H; [ exists (ip'); reflexivity | ].  
+  assert (exists ip'', get_link (bg:=b) ip'' = get_link (bg:=b) ip') as H; 
+    [ exists (ip'); reflexivity | ].  
   destruct (get_link (bg:=b) ip') as [o'|e'].
   + left. exact o'.
   + right. exists e'. (*le GOAL*) 

src/ListSpec.v

@@ -7,7 +7,7 @@ Import ListNotations.
 Ltac disjunction H := destruct H as [ H | H ].
 
 Definition cons_type {T} h t (e : { e : T | In e t }) : { e : T | In e (h :: t)} :=
-  let (e, H__e) := e in exist _ e (in_cons h e t H__e).
+  let (e, H_e) := e in exist _ e (in_cons h e t H_e).
 
 Fixpoint onto {T : Type} (l : list T) : list { e : T | In e l } :=
   match l with